Lean Graph Search for Formal Theorem Proving
Yihan Xu, Jia-Chen Gu, Junyi Zhang, Di Wu, Haikang Deng, Po-Nien Kung, Kai-Wei Chang, Amit Sahai, Wei Wang, Nanyun Peng
cs.LG
Oct 15, 2026 · v1
TL;DR
Builds a premise-retrieval graph from Mathlib declaration dependencies and uses it in an LLM proving loop driven by Lean compiler feedback.
Abstract
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.
Problem
Lemma retrieval systems for Lean match library declarations to a query by semantic similarity. They make little use of multi-hop dependencies among declarations, so they can miss supporting lemmas that are not lexically similar to the target theorem.
Approach
LeanGraphSearch uses static analysis with jixia to build a directed dependency graph over Mathlib declarations, with an edge from each declaration to the premises its type and value reference. Semantic seeds come from embedding retrieval plus reranking. Personalized PageRank then propagates relevance from the seeds to their dependencies, and the merged candidates are reranked against the original query. The retriever is exposed as a search tool inside an iterative LLM proving loop that uses Lean compiler diagnostics and an optional failure memory.
Results
On MathlibQR, Recall@100 rises from 82.7% (LeanSearch v2) to 94.7%. On MathlibMPR, Covered@20 rises from 39.1% to 42.8%. In end-to-end proving on FATE-H, MathlibMPR-Prop and Lean-IMO-Bench, pass rates are generally higher than LeanSearch v2 at similar or lower cost, reaching 81 vs 73 on FATE-H at pass@32.
| Method | nDCG@10 | Recall@10 | Recall@100 |
|---|
| LeanExplore | 0.393 | 0.569 | 0.789 |
| LeanFinder | 0.533 | 0.698 | 0.875 |
| LeanSearch v2 | 0.616 | 0.765 | 0.827 |
| LeanGraphSearch | 0.629 | 0.794 | 0.947 |
MathlibQR retrieval (standard mode)