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.
Figures & tables
Figure 1: Dependency-guided retrieval with LeanGraphSearch . (a) An illustration of the dependency graph, showing how semantically retrieved declarations (blue) lead to supporting premises (green) through shared and multi-hop dependencies. (b) Selected retrieval and proving results. Gains are reported in percentage points relative to LeanSearch v2.
Figure 2: Overview of LeanGraphSearch . (a) Dependency graph construction ( Section 3.2 ). Static analysis with jixia extracts references from Mathlib declarations to construct a directed graph G . (b) Graph-based retrieval ( Section 3.3 ). It first retrieves semantic seeds using semantic embeddings, then expands the candidate set by traversing the dependency graph. Seed and graph-expanded candidates are merged and reranked to select the final top- K declarations.
nDCG@ k
Recall@ k
Method
1
5
10
10
50
100
LeanExplore
0.246
0.358
0.393
0.569
0.743
0.789
LeanFinder
0.370
0.514
0.533
0.698
0.824
0.875
LeanSearch v2 (standard mode)
0.472
0.596
0.616
0.765
0.821
0.827
LeanGraphSearch (standard mode)
0.473
0.604
0.629
0.794
0.899
0.947
Table 1: Query-to-declaration retrieval on the 810-query fair subset of MathlibQR. LeanExplore and LeanFinder are quoted from Gao et al. (2026) . The best result in each column is bold .
Method
Recall@ k (group)
Covered@ k
5
10
20
30
50
5
10
20
30
50
INF-X-Retriever
21.2
28.2
33.9
40.0
42.6
15.9
18.8
21.7
24.6
24.6
ReasonIR
23.9
26.9
33.3
35.6
43.8
17.4
18.8
20.3
21.7
30.4
DIVER
27.7
38.0
46.6
52.8
55.0
18.8
24.6
29.0
33.3
37.7
ReProver
3.0
5.5
7.6
8.8
10.3
0.0
1.4
2.9
4.3
4.3
LeanPremise
4.1
4.8
8.0
9.9
11.5
1.4
1.4
4.3
4.3
5.8
Table 2: Global premise retrieval on MathlibMPR. The two evaluated method rows are arithmetic means over Gemini 3.1 Pro and Claude Sonnet 5. Baseline results are quoted from Gao et al. (2026) .
Retrieval condition
pass@ 8
pass@ 16
pass@ 32
Relative cost
Failure Memory Disabled
No retrieval
35
42
47
1.00×
LeanSearch v2 (standard mode)
49
61
70
1.11×
LeanGraphSearch (standard mode)
53
69
71
1.09×
LeanSearch v2 (reasoning mode)
52
68
73
1.41×
LeanGraphSearch (reasoning mode)
56
70
75
1.37×
Table 3: Proving results on FATE-H , grouped by whether failure memory is enabled. Relative cost is the full-budget API cost normalized by no retrieval within each group. The best and second best results in each group are shown in bold and underlined , respectively.
Retrieval condition
pass@ 8
pass@ 16
pass@ 32
Relative cost
Failure Memory Disabled
No retrieval
15
18
23
1.00×
LeanSearch v2 (standard mode)
31
35
39
0.82×
LeanGraphSearch (standard mode)
32
38
41
0.78×
LeanSearch v2 (reasoning mode)
33
37
41
1.01×
LeanGraphSearch (reasoning mode)
33
38
39
1.06×
Table 4: Proving results on MathlibMPR-Prop , grouped by whether failure memory is enabled.
Retrieval condition
Basic Set ( n=30 )
Advanced Set ( n=30 )
pass@ 8
pass@ 16
pass@ 32
Rel. cost
pass@ 8
pass@ 16
pass@ 32
Rel. cost
Failure Memory Disabled
No retrieval
12
16
16
1.00×
7
7
8
1.00×
LeanSearch v2 (standard mode)
15
15
18
1.49×
4
8
9
1.82×
LeanGraphSearch (standard mode)
16
17
21
1.40×
5
9
10
1.88×
LeanSearch v2 (reasoning mode)
14
16
21
2.04×
7
9
10
2.56×
Table 5: Proving results on Lean-IMO-Bench , grouped by whether failure memory is enabled.
Figure 3: Cost efficiency on theorem proving. LS = LeanSearch, LGS = LeanGraphSearch , Std. = Standard Mode, Reas. = Reasoning Mode. For each of the 10 configurations, we compute total API cost divided by the number of solved problems on the union of 210 theorem-proving instances. Solved counts are measured by pass@32. Lower values indicate better cost efficiency.
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
Mathematical knowledge is organized around statements and their dependencies, but this structure is exposed unevenly: informal papers cite mostly at the document level, while formal libraries record fine-grained dependencies over a much smaller body of mathematics. We introduce TheoremGraph, a unified statement-level dependency graph spanning both informal and formal mathematics. On the informal side, we parse 11.7M theorem-like environments from mathematics arXiv and recover 18.3M candidate directed dependencies, each labeled by the extractor that proposed it so downstream users can trade coverage for precision. On the formal side, we release LeanGraph, a Lean 4 elaborator-level extractor producing 388,105 declaration nodes and 11.3M typed edges across 25 Lean projects. We bridge the two graphs by embedding generated natural-language slogans into a shared semantic space, linking related statements across papers and across the informal/formal divide; an LLM judge affirms 47,952 such matches above a 0.8 cosine floor, with the judge-acceptance rate rising from 48% across the floor to 87% in the >=0.9 tier. On formal concept retrieval, our name-and-signature representation with graph expansion comes within 0.5pp of LeanSearch v2's reranked Recall@10 (0.775 vs. 0.780) without an LM reranker. We release the dataset, extractors, HTTP API, and MCP interface as infrastructure for mathematical search, attribution, and retrieval-augmented reasoning, available at theoremsearch.com and huggingface.co/datasets/uw-math-ai/theorem-matching.
We introduce Lean Finder V2, a semantic search framework for Mathlib that disambiguates user queries through complementary model-level adversarial training and input-level query rewriting. Human mathematicians and coding agents rarely search Mathlib by providing detailed context. In practice, they query short properties, notation, aliases, or hypotheses, leaving much of the intended mathematics implicit. In contrast, existing Mathlib search engines unrealistically assume context-rich queries. The scarcity of real-world short queries paired with ground-truth Mathlib statements makes this ambiguity even more intractable. We argue that this is essentially a data problem. Through adversarial training, we scale up the generation of labeled short and ambiguous queries, and learn to disambiguate user queries at both model-level fine-tuning and input-level query rewriting. On the human-curated MathlibQR benchmark, our Lean Finder V2 sets a new state of the art, with at least 11% relative improvement over the previous best Mathlib semantic search engines. On top of our state-of-the-art retriever, optimized query rewriting further improves MathlibQR retrieval. On unlabeled queries from human and coding-agent interactions, Lean Finder V2 is ranked as the strongest system. Integrated with Claude Code, Lean Finder V2 improves proof success on downstream theorem-proving task. Lean Finder V2 is available at: https://leanfinder.github.io/
Jialin Lu, Xiaoyu Liu, Hengrui Luo +5
Simon Fraser University · Rice University · University of Pittsburgh