DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving

Zixuan Chen; Wenyuan Jiang; Junling Wang; Mrinmaya Sachan; Yinya Huang

cs.LOOct 30, 2026

DAPS: Dependency-Aware Premise Selection for LLM Theorem Proving

Authors: Zixuan Chen, Wenyuan Jiang, Junling Wang, Mrinmaya Sachan, Yinya Huang

Organizations: ETH Zurich · ETH Zurich, ETH AI Center

Abstract

LLM-based theorem proving in Lean 4 has advanced rapidly, but provers are difficult to leverage newly contributed lemmas, because retrieval skews toward popular foundational lemmas, leaving the right premises buried among hundreds of thousands of candidates. Existing neural selectors rank candidates by semantic similarity, with three intrinsic limitations: frequency-skewed retrieval, isolated pairwise ranking, and degradation on out-of-distribution queries such as competition problems and informal language. Given that mathematics is structured by dependencies rather than similarities, we restore this signal to both the training data and the model. We curate two underused dependency resources. We conduct the first systematic mining of 53 Lean Blueprint projects, a previously untapped corpus of 3,805 manually curated informal+formal nodes that capture rare, research-level premises absent from Mathlib4. We further pair it with the extraction of comprehensive, typed, multi-level Mathlib4 dependencies. We then introduce DAPS, a dependency-aware premise selector with a structural neighborhood encoder, a group-level contrastive objective, and a Mathlib-then-Blueprint adaptation procedure. DAPS reaches mean Recall@32 of 89.25 on Mathlib4-Heldout (+11.41 over the strong selector LeanHammer), and maintains this lead on two out-of-distribution benchmarks. Further experiments demonstrate that DAPS premises improve theorem proving on miniF2F and IMO-ProofBench. Project page: https://daps-eth.github.io/.

Figures & tables

Figure 1: One dependency graph spanning Mathlib4 (left) and a representative Blueprint project (right). The two resources differ in density and composition. Mathlib4 averages 24 edges per node with strong directional asymmetry across node types, while Blueprint dependencies are much sparser, averaging 1.2, but carry research-level out-of-Mathlib4 declarations and informal L a T e X signals.

Panel of Figure 2 — Figure 2: Mathlib4’s dependency graph carries a rich, asymmetric, frequency-skewed structure. (a) 15 typed edge categories totaling 6.5M edges. (b) Average in- vs. out-degree per node category (bubble area $\propto\log_{10}\#\text{nodes}$ ). Statements (red) sit at the high-out/low-in extreme, foundational type - defining constructs (blue) at the opposite extreme.

# Projects	53
# Nodes / # Edges	3,805 / 4,651
Formal vs. informal nodes	2,728 (71.7%) / 1,077 (28.3%)
Project size: median / mean / range	35 / 71.8 / 6–525
Fully-formalized projects	14
Informal-majority projects	14

Table 1: Mined Lean Blueprint corpus (full per-project listing in Appendix E.2 ).

Source	#Train	#Val	Test slices (#queries)
Mathlib4	275,842	2,000	Mathlib4-Heldout (1,000), Mathlib4-Random (1,000)
Blueprints	1,880	235	DAPS -Blueprint (236)
DAPS -Collection	–	–	DAPS -Collection (1,000)

Table 2: Training and evaluation data.

Figure 3: Composition of the mined Blueprint corpus. The top-15 projects are shown individually, while the remaining 38 are aggregated into the bottom bar. Bars are divided into formal nodes (green; statements with Lean proofs) and informal nodes (gray; L a T e X -only statements, sometimes with informal proofs).

Method	Mathlib4-R	Mathlib4-H	DAPS -Coll.	DAPS -BP
MePo ( Meng et al., 2006 )	$18.84{\pm}0.04$	$11.06{\pm}0.01$	$0.75{\pm}0.00$	–
ReProver ( Yang et al., 2023 )	$36.97{\pm}0.00$	$43.48{\pm}0.00$	$1.24{\pm}0.00$	$32.04{\pm}0.00$
LeanHammer ( Zhu et al., 2025 )	$73.99{\pm}0.00$	$77.84{\pm}0.00$	$3.19{\pm}0.00$	$40.42{\pm}0.00$
Qwen3-Embedding-8B ( Zhang et al., 2025b )	$15.25{\pm}0.00$	$9.92{\pm}0.00$	$0.36{\pm}0.00$	$13.07{\pm}0.00$
DAPS	$\mathbf{80.68{\pm}0.668}^{\,\dagger}$	$\mathbf{89.25{\pm}0.170}^{\,\dagger}$	$\mathbf{23.53{\pm}0.757}^{\,\dagger}$	$\mathbf{50.08{\pm}0.889}^{\,\ddagger}$

Table 3: Recall@32 (mean

\pm

standard deviation over three runs) across all four benchmarks. For fair comparison, ReProver, LeanHammer, and Qwen3-Embedding-8B are retrained on the same Mathlib dependency data using their published recipes. MePo is symbolic and used as released.

\dagger

: Mathlib-only model.

\ddagger

: After Blueprint continual training. Mathlib4-R: Mathlib4-Random. Mathlib4-H: Mathlib4-Heldout. DAPS -Coll.: DAPS -Collection. DAPS -BP: DAPS -Blueprint.

Model	LeanExplore	LeanSearch	Qwen3	DAPS	$\Delta$ %
Qwen3-235b ( Yang et al., 2025 )	18.45	17.01	19.08	21.25	11.37
DeepSeek-V3.1 ( DeepSeek-AI, 2024 )	11.96	12.38	13.75	13.90	1.09
kimi-k2-instruct ( Bai et al., 2025 )	8.66	8.26	8.27	9.08	4.85
Gemini-3.6-Flash 5 5 5 https://deepmind.google/models/model-cards/gemini-3-6-flash/	46.13	44.04	45.51	48.69	5.55

Table 4: Downstream utility performance. Pass@8 of different LLMs on IMO-ProofBench ( Luong et al., 2025a ) using premises from compared premise selectors. In this table, we strictly follow the original grading prompts from the IMO-ProofBench paper and use the identical grading model. Qwen3: Qwen3-Embedding-8B.

\Delta

\Delta

% vs best baseline

	Goedel-Prover-V2-8B			DeepSeek-Prover-V2-7B
	pass@1	pass@2	pass@4	pass@1	pass@2	pass@4
w/o premises	36.48	43.62	49.90	34.07	42.23	48.23
LeanExplore	40.37	47.18	52.36	36.73	44.29	48.72
LeanSearch	39.19	46.05	51.43	34.32	42.21	47.32
Qwen3-Embedding-8B	39.86	46.41	51.84	35.09	42.86	47.68
MePo	37.92	44.74	50.60	35.60	43.06	47.75

Table 5: Formal theorem proving results on miniF2F-test ( Zheng et al., 2021 ) . Bold and underline are the best and the second-best results, respectively.

Panel of Figure 4 — Figure 4: (a) Recall@ $K$ on DAPS -Blueprint for $K\in\{8,16,32\}$ . (b) Per-pair hit@32 by premise frequency on Mathlib4-Random. (c) Per-pair hit@32 by premise frequency on Mathlib4-Heldout.

Appendix figures & tables29 assets

Supplementary material from the paper’s appendix.

Appendix

Workload	Hardware	#Devices	Runtime	Compute
Stage 1: text encoder warm-up	GH200 cluster	16	$\leq$ 12 h	$\leq$ 192 GPU-h
Stage 2: structural fusion training	GH200 cluster	16	$\leq$ 24 h	$\leq$ 384 GPU-h
Blueprint continual training	MacBook Pro (M4 Max)	1	$\leq$ 3 h	$\leq$ 3 machine-h
Total (cluster training)				$\leq$ 408 GPU-h
Total (local training)				$\leq$ 3 machine-h

Appendix

Table 6: Compute consumed by the reported training workloads. Cluster runtimes are aggregated GPU-hours on NVIDIA GH200. The Blueprint adaptation stage is reported as machine-hours since it runs on a single local workstation.

Figure 5: The top 10% of nodes attract 56% of all incoming edges (category-aggregate approximation; per-node curve is steeper).

Table 12

Node Field	Definition
name	Fully qualified Lean name (e.g., AddConstMap.instFunLike ) or the synthetic file_⁢ identifiers we create from the filesystem.
category	Underlying ConstantInfo tag ( theorem , def , instance , inductive , structure , class , constructor , recursor , etc.).
line / column	Start position from findDeclarationRanges? , measured in the source .lean file.
doc	Docstring preceding the declaration; null when absent.
signature	Canonical type with all binders and constants spelled out.
isProp	Flags declarations whose type lives in Prop .

Appendix

Table 9: Description of node fields.

Edge Field	Definition
source_name / target_name	The name entry of source/target node of the edge.
category	Semantic label chosen based on the source and the target’s subcategory . Conventions: CONTAINS for file $\to$ declaration, IMPORTS for file $\to$ file, DEPENDS_ON for anything targeting a theorem/lemma/axiom (including derived variants), and USES<CATEGORY> (e.g., USES_CLASS , USES_INSTANCE_DERIVED , USES_STRUCTURE ) for everything else.
explicit	Whether a dependency appears in the explicit argument positions of the source declaration. It is True when the referenced constant is used only through explicit parameters( i.e. binderInfo = .default ). It is False when the dependency arises solely via implicit arguments, including implicit {} binders or typeclass instance parameters [] .
direct	True if the dependency can be obtained from calling function getUsedConstantsAsSet in ConstantInfo ). False if it is obtained through further unfolding the direct dependencies of auxiliary lemmas.
could_skip	True if the target node in_blacklist .

Appendix

Table 10: Description of edge fields.

Node Categories	#node	avg.	max #in-degree	total #in-degree
class	2,126	348.20	62,237	740,276
structure	3,260	174.95	24,449	570,325
class_derived	11,472	148.51	49,867	1,703,655
instance_derived	1,912	79.71	16,527	152,413
inductive	290	60.77	2,474	17,622
instance	22,462	58.24	32,159	1,308,114

Appendix

Table 11: In-degree distribution by node category (sorted by average out-degree).

Node Categories	#node	avg.	max #out-degree	total #out-degree
file	6,726	43.70	684	293,910
example_derived	1	37.00	37	37
lemma	39,832	31.08	395	1,237,896
theorem	116,096	26.85	474	3,116,776
lemma_derived	3,918	25.36	259	99,369
attribute_derived	3	20.33	25	61

Appendix

Table 12: Out-degree distribution by node category (sorted by average out-degree).

Project	#Nodes	#Edges	#Formal	#Informal
AlexKontorovich/PrimeNumberTheoremAnd	525	694	487	38
RemyDegenne/brownian-motion	458	732	298	160
teorth/pfr	218	403	214	4
teorth/equational_theories	214	185	145	69
firsching/FormalBook	189	93	55	134
florisvandoorn/carleson	179	213	175	4

Appendix

Table 13: Per-project statistics of the mined Lean Blueprint corpus, sorted by node count. Project names link to the original blueprint.

	$\ell$	$m$	$n$	$k_{t}$	$k_{g}$	$k_{c}$
Mathlib4 encoder	32	300	64	0	3	all
Mathlib4 structural fusion	32	300	64	30	30	1,500
Blueprint continual training	all	33	33	15	45	960

Appendix

Table 14: Training hyperparameters.

\ell

= max positives per query (top-

\ell

after category-priority sort);

m,n

= dynamic subgraph sampling budget (random sample/keep after FFN scoring);

k_{t},k_{g},k_{c}

= numbers of temporal/global/cross-batch negatives per query.

Panel of Figure 6 — Figure 6: Prompt for in-context premise use.

Panel of Figure 7 — Figure 7: Baseline prompt without retrieved premises.

Method	Precision@16	Recall@16	F1@16	Precision@32	Recall@32	F1@32
MePo	$8.02{\pm}0.01$	$14.14{\pm}0.03$	$8.95{\pm}0.02$	$5.72{\pm}0.01$	$18.84{\pm}0.04$	$7.93{\pm}0.02$
ReProver	$13.01{\pm}0.00$	$26.97{\pm}0.00$	$15.68{\pm}0.00$	$9.58{\pm}0.00$	$36.97{\pm}0.00$	$13.99{\pm}0.00$
LeanHammer	$35.56{\pm}0.00$	$61.13{\pm}0.00$	$40.57{\pm}0.00$	$23.45{\pm}0.00$	$73.99{\pm}0.00$	$32.81{\pm}0.00$
Qwen3-Embedding-8B	$5.84{\pm}0.00$	$11.54{\pm}0.00$	$6.87{\pm}0.00$	$3.91{\pm}0.00$	$15.25{\pm}0.00$	$5.68{\pm}0.00$
DAPS	$\mathbf{37.60{\pm}0.51}$	$\mathbf{66.01{\pm}0.88}$	$\mathbf{43.49{\pm}0.62}$	$\mathbf{25.71{\pm}0.25}$	$\mathbf{80.68{\pm}0.67}$	$\mathbf{36.01{\pm}0.35}$

Appendix

Table 15: Full retrieval results on Mathlib4-Random (mean

\pm

standard deviation over three runs).

Method	Precision@16	Recall@16	F1@16	Precision@32	Recall@32	F1@32
MePo	$4.30{\pm}0.01$	$7.98{\pm}0.01$	$5.12{\pm}0.01$	$2.98{\pm}0.01$	$11.06{\pm}0.01$	$4.37{\pm}0.01$
ReProver	$12.13{\pm}0.00$	$32.32{\pm}0.00$	$16.70{\pm}0.00$	$8.49{\pm}0.00$	$43.48{\pm}0.00$	$13.64{\pm}0.00$
LeanHammer	$28.02{\pm}0.00$	$67.33{\pm}0.00$	$37.41{\pm}0.00$	$16.98{\pm}0.00$	$77.84{\pm}0.00$	$26.59{\pm}0.00$
Qwen3-Embedding-8B	$3.21{\pm}0.00$	$6.74{\pm}0.00$	$4.03{\pm}0.00$	$2.34{\pm}0.00$	$9.92{\pm}0.00$	$3.58{\pm}0.00$
DAPS	$\mathbf{32.47{\pm}0.06}$	$\mathbf{78.74{\pm}0.19}$	$\mathbf{43.67{\pm}0.10}$	$\mathbf{19.67{\pm}0.05}$	$\mathbf{89.25{\pm}0.17}$	$\mathbf{30.79{\pm}0.07}$

Appendix

Table 16: Full retrieval results on Mathlib4-Heldout (mean

\pm

standard deviation over three runs).

Method	Precision@16	Recall@16	F1@16	Precision@32	Recall@32	F1@32
MePo	$0.74{\pm}0.00$	$0.53{\pm}0.00$	$0.60{\pm}0.00$	$0.53{\pm}0.00$	$0.75{\pm}0.00$	$0.60{\pm}0.00$
ReProver	$1.05{\pm}0.00$	$0.75{\pm}0.00$	$0.85{\pm}0.00$	$0.92{\pm}0.00$	$1.24{\pm}0.00$	$1.03{\pm}0.00$
LeanHammer	$2.94{\pm}0.00$	$1.98{\pm}0.00$	$2.32{\pm}0.00$	$2.51{\pm}0.00$	$3.19{\pm}0.00$	$2.76{\pm}0.00$
Qwen3-Embedding-8B	$0.34{\pm}0.00$	$0.24{\pm}0.00$	$0.27{\pm}0.00$	$0.26{\pm}0.00$	$0.36{\pm}0.00$	$0.29{\pm}0.00$
DAPS	$\mathbf{26.28{\pm}0.48}$	$\mathbf{13.84{\pm}0.24}$	$\mathbf{18.00{\pm}0.32}$	$\mathbf{22.52{\pm}0.73}$	$\mathbf{23.53{\pm}0.76}$	$\mathbf{22.88{\pm}0.74}$

Appendix

Table 17: Full retrieval results on DAPS -Collection (mean

\pm

standard deviation over three runs).

Method	Precision@16	Recall@16	F1@16	Precision@32	Recall@32	F1@32
ReProver	$2.44{\pm}0.00$	$25.37{\pm}0.00$	$4.36{\pm}0.00$	$1.55{\pm}0.00$	$32.04{\pm}0.00$	$2.93{\pm}0.00$
LeanHammer	$2.97{\pm}0.00$	$31.36{\pm}0.00$	$5.32{\pm}0.00$	$1.96{\pm}0.00$	$40.42{\pm}0.00$	$3.70{\pm}0.00$
Qwen3-Embedding-8B	$1.11{\pm}0.00$	$11.02{\pm}0.00$	$1.97{\pm}0.00$	$0.65{\pm}0.00$	$13.07{\pm}0.00$	$1.219{\pm}0.00$
DAPS	$\mathbf{3.83{\pm}0.03}$	$\mathbf{42.21{\pm}0.75}$	$\mathbf{6.87{\pm}0.06}$	$\mathbf{2.42{\pm}0.05}$	$\mathbf{50.08{\pm}0.89}$	$\mathbf{4.55{\pm}0.10}$

Appendix

Table 18: Full retrieval results on DAPS -Blueprint (mean

\pm

standard deviation over three runs). MePo does not support the Blueprint candidate collection.

Query formalization	Pass@4
Gemini-3-Pro	46.55
Goedel-Formalizer-V2-32B	47.50
Manual formalization	48.27

Appendix

Table 19: Effect of the informal-query formalizer on IMO-ProofBench. The proof generator is Gemini-3.6-Flash in every row, and the metric is Pass@4.

Variant	Mathlib4-R	Mathlib4-H	DAPS -Coll.
(a) Full configuration
DAPS (warmed-up MGTE encoder, DySS, 2-hop bidirectional, all node categories)	79.63	89.31	24.38
(b) Encoder ablations
$-$ encoder warm-up	74.30	81.08	15.63
$-$ structural fusion (MGTE encoder only)	56.29	43.85	5.53
$-$ MGTE encoder $\to$ warmed-up ReProver/ByT5	74.20	81.72	1.08

Appendix

Table 20: Component ablation of DAPS . Recall@32 results are reported. Rows progressively remove components from the full configuration (top row) to isolate each component’s contribution. Encoder ablations vary the text encoder backbone. Subgraph ablations vary the dependency-graph signal that DAPS uses. DySS : Dynamic subgraph sampling. TLD-only : Restricted node categories of theorem , lemma , and definition . Mathlib4-R : Mathlib4-Random. Mathlib4-H : Mathlib4-Heldout. DAPS -Coll. : DAPS -Collection. Unlike the main retrieval table, these diagnostic ablations are fixed-seed runs and are reported as point estimates.

Failure mode	Symptom	Rep. case
Type over-generalization	DAPS retrieves typeclass instances on a type that shares the relevant typeclass with the target, but is not the target itself.	App. 16
Lexical sibling drift	When the query is a modifier-prefixed or -suffixed sibling of an in-corpus lemma, DAPS retrieves thematically related premises rather than the near-identical sibling.	App. 17
Topical subgraph drift	DAPS resolves the correct project, but selects the wrong topical subgraph when several thematically adjacent clusters compete.	App. 18

Appendix

Table 21: Failure modes observed in our case studies, with one representative case per mode (full case studies in Appendices 16 – 18 ).

Panel of Figure 8 — Figure 8: A training instance for semantic encoder warm up.

Panel of Figure 9 — Figure 9: A training instance for Mathlib4 pretraining.

Panel of Figure 10 — Figure 10: A training instance for Blueprint continual training.

Panel of Figure 11 — Figure 11: Case study from the teorth/pfr Blueprint project. ✓ marks premises in the gold positive set. Premise names follow the PFR Blueprint label scheme.

Panel of Figure 12 — Figure 12: Case study from the AlexKontorovich/PrimeNumberTheoremAnd Blueprint project. ✓ marks premises in the gold positive set. Premise names follow the PFR Blueprint label scheme.

Panel of Figure 13 — Figure 13: Case study from the DAPS -Collection benchmark (a Lean Workbook problem). ✓ marks premises in the gold positive set. Premise names follow Mathlib4 declaration paths.

Panel of Figure 14 — Figure 14: Case study from the Mathlib4-Held-out benchmark. ✓ marks premises in the gold positive set. Premise names are Mathlib4 declaration paths.

Panel of Figure 15 — Figure 15: Case study from the Mathlib4-Random benchmark. ✓ marks premises in the gold positive set. Premise names are Mathlib4 declaration paths.

Panel of Figure 16 — Figure 16: Failure case study from DAPS -Collection (a Lean Workbook problem). ✓ marks premises in the gold positive set. DAPS retrieves zero gold premises in its top-32 on this query, while LeanHammer and ReProver each retrieve two. Premise names are Mathlib4 declaration paths.

Panel of Figure 17 — Figure 17: Failure case study from DAPS -Blueprint (the brownian-motion project). ✓ marks premises in the gold positive set. DAPS retrieves zero gold premises in its top-32 here, while LeanHammer and ReProver each retrieve one (the lexically near-identical A_uniform_integrable ). The case illustrates a second failure mode for DAPS . When the gold premise shares strong lexical similarity with the query name, text-only baselines exploit the direct match, whereas DAPS drifts across the global Blueprint corpus along thematic lines.

Panel of Figure 18 — Figure 18: Failure case study from DAPS -Blueprint (the PrimeNumberTheoremAnd project). ✓ marks premises in the gold positive set. DAPS retrieves zero gold premises in its top-32, while LeanHammer retrieves the single gold premise at position 6, and ReProver also fails. The case reveals a within-project topical drift for DAPS . Structural features can resolve the right project but pick the wrong topical subgraph when several thematically adjacent clusters exist.

Large Language Model-Guided Theorem Proving

See all 56 papers

May 13, 2026

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

Proving theorems in Lean 4 often requires identifying a scattered set of library lemmas whose joint use enables a concise proof -- a task we call global premise retrieval. Existing tools address adjacent problems: semantic search engines find individual declarations matching a query, while premise-selection systems predict useful lemmas one tactic step at a time. Neither recovers the full premise set an entire theorem requires. We present LeanSearch v2, a two-mode retrieval system for this task. Its standard mode applies a hierarchy-informalized Mathlib corpus with an embedding-reranker pipeline, achieving state-of-the-art single-query retrieval without domain-specific fine-tuning (nDCG@10 of 0.62 vs. 0.53 for the next-best system). Its reasoning mode builds on standard mode as its retrieval substrate, targeting global premise retrieval through iterative sketch-retrieve-reflect cycles. On a 69-query benchmark of research-level Mathlib theorems, reasoning mode recovers 46.1% of ground-truth premise groups within 10 retrieved candidates, outperforming strong reasoning retrieval systems (38.0%) and premise-selection baselines (9.3%) on the same benchmark. In a controlled downstream evaluation with a fixed prover loop, replacing alternative retrievers with LeanSearch v2 yields the highest proof success (20% vs. 16% for the next-best system and 4% without retrieval), confirming that retrieval quality propagates to proof generation. We have open-sourced all code, data, and benchmarks. Code and data: https://github.com/frenzymath/LeanSearch-v2 . The standard mode is publicly available with API access at https://leansearch.net/ .

Guoxiong Gao, Zeming Sun, Jiedong Jiang +5

School of Mathematical Sciences, Peking University · 2IQuest Research · 3Research Institute for Mathematical Sciences, Kyoto University +5

Lean Theorem Proving Evidence Retrieval

Ask PDF

Oct 15, 2026

Lean Graph Search for Formal Theorem Proving

Retrieving relevant lemmas is crucial for formal theorem proving, enabling provers to build machine-checkable proofs from established mathematical results. Recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, but make limited use of multi-hop dependencies among declarations. These dependencies can reveal supporting lemmas that are not necessarily lexically similar to the target theorem but recur in proofs of related problems. To this end, we propose LeanGraphSearch, a graph-based retrieval method for Lean 4 that constructs a graph from Mathlib's forward dependencies and traverses it to uncover supporting lemmas through multi-hop dependency chains. Specifically, LeanGraphSearch links each declaration to the premises it depends on, uses a graph-based ranking algorithm to propagate relevance from semantically matched declarations to their dependencies, and reranks the expanded candidates against the original query. Across two mathematical retrieval benchmarks, LeanGraphSearch improves recall by up to 12% over the strongest baseline, LeanSearch v2, on MathlibQR and increases coverage of complete annotated proof routes on MathlibMPR, covering up to 3.7% of extra groups. More importantly, we evaluate whether these retrieval gains translate into improved end-to-end theorem proving by integrating LeanGraphSearch into an iterative proving loop guided by Lean feedback. Across three theorem proving benchmarks, LeanGraphSearch improves pass rate at {8, 16, 32} reflection turns by as much as 40% compared to vanilla prover and at most 10% compared to LeanSearch v2, showing higher accuracy-cost efficiency. These findings highlight the value of dependency graph search for theorem proving and motivate further research on structure-aware search for proof discovery.

Yihan Xu, Jia-Chen Gu, Junyi Zhang +7

University of California, Los Angeles

Graph-Based Retrieval Lean Theorem Proving Automated Theorem Proving Multi-Hop Reasoning

Ask PDF

Jun 8, 2026

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.

QuocViet Pham, Elvir Karimov, Andrey Galichin +1

Skolkovo Institute of Science and Technology · HSE University · Sberbank +1

Mathematical Reasoning Benchmarks LLM Evaluation Automated Theorem Proving Benchmark Design Lean Theorem Proving Large Language Model-Guided Theorem Proving

Ask PDF

Abstract

Large Language Model-Guided Theorem Proving

Explore similar work

LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving

Lean Graph Search for Formal Theorem Proving

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics