LeanGraphSearch: Dependency Graph Search Boosts Theorem Proving Retrieval and Pass Rates

Title

LeanGraphSearch: Dependency Graph Search Boosts Theorem Proving Retrieval and Pass Rates

Meta Description

LeanGraphSearch proposes a dependency-graph-based retrieval method for Lean 4 theorem proving, improving Mathlib recall by up to 12% via multi-hop dependency propagation and boosting end-to-end pass rates by up to 40% over standard provers.

Article Content

The hard part of formal theorem proving is often not the reasoning itself, but finding the right lemmas to use from a massive mathematical library. Whether the retrieved lemmas are relevant directly determines whether the prover can construct a machine-verifiable proof. Most existing retrieval systems perform semantic matching between library declarations and the target theorem or its current proof step, but ignore the multi-hop dependencies between declarations—those supporting lemmas that are not literally similar to the target theorem yet repeatedly appear in proofs of related problems. LeanGraphSearch is a graph-based retrieval method proposed precisely to fill this gap.

The Blind Spot of Retrieval: Why Literal Matching Falls Short

Traditional retrieval assumes that "semantic similarity" roughly equals "usefulness." In Lean 4's Mathlib, proving a target theorem often requires calling a chain of indirectly dependent lemmas, which share very little vocabulary with the target theorem yet form the key chain of the proof. Semantic matching against the target theorem alone struggles to recall these "deeply buried" lemmas. The dependency graph offers another clue: if a declaration is highly relevant to the target theorem, then its premises are likely worth considering too, and those premises in turn depend on declarations one layer deeper.

LeanGraphSearch's core claim is that proof discovery is fundamentally a structure-aware search problem, not merely a text similarity ranking problem. Dependencies turn loose literal matches into a propagatable relevance signal.

Mathlib is Lean 4's mathematical library and one of the largest unified libraries in formal mathematics today, covering a vast number of theorems and structures from basic algebra and analysis to topology and number theory. It contains hundreds of thousands of declarations (definitions, theorems, lemmas, etc.), each linked via dependencies to the premises it uses. Because of this scale, neither human memory nor purely semantic retrieval can quickly locate suitable lemmas during proving. Mathlib's declarations are highly modular: a high-level theorem often depends on several intermediate lemmas, which in turn depend on more basic results, forming deep chains. This organization makes dependency-graph-based retrieval possible, and also implies a systematic gap between "semantic similarity" and "proof usefulness."

Multi-hop dependencies refer to indirect premises reachable from the target declaration via one or more dependency edges. For example, target theorem A directly depends on B, B depends on C, and C depends on D; when proving A, D may appear as an auxiliary lemma, yet A and D may have extremely low literal similarity. Traditional semantic retrieval typically performs only a single round of similarity ranking between A and candidate declarations, so it easily misses key supporting lemmas like C and D that lie deep in the dependency chain. The purpose of multi-hop propagation is precisely to exploit the structural assumption that "if A is relevant, then A's premises are also worth considering," gradually spreading relevance from anchors along dependency edges, thereby recalling candidates that single-round matching cannot cover.

Method: Starting from Links, Doing Multi-Hop Propagation and Reranking

LeanGraphSearch builds a graph for Lean 4 from Mathlib's forward dependencies: each declaration links to the premises it depends on. On this graph, the algorithm first performs a semantic match to find declarations semantically close to the target query as starting points, then uses a graph ranking algorithm to propagate relevance from these starting points along dependency edges outward to their premises, thereby expanding to candidates that are literally dissimilar but structurally relevant. Finally, the system reranks the expanded candidate set against the original query and outputs the final retrieval result.

This pipeline can be summarized in three steps: semantic matching to locate anchors, dependency graph propagation to dig out multi-hop supporting lemmas, and reranking to control precision. Compared with direct retrieval, it relies more on the library's own structural information rather than simply stacking larger semantic models.

The role of the graph ranking algorithm here is to treat the initial semantic matching scores as seed signals on nodes and then propagate scores to neighboring nodes according to the structure of the dependency graph. Common approaches include Personalized PageRank, random walks, or weighted propagation with decay: the closer a node is semantically to the query and the shorter its dependency path to highly relevant nodes, the higher its final score. Unlike pure semantic similarity, graph ranking introduces a structural prior—namely, that "premises depended on by relevant declarations also tend to be relevant." In LeanGraphSearch, propagation follows forward dependency edges (declarations point to their premises), so scores spread from semantic anchors toward deeper premises. The propagated candidate set is then reranked against the original query, effectively using structural signals to correct semantic ranking, balancing recall and precision.

In the forward dependency graph, edges go from a declaration to the premises it references, aligning with the direction in a proof of decomposing "from goal to subgoal." In contrast, a reverse dependency graph would point from premises to the declarations that use them. The reason for choosing the forward graph is that the retrieval goal is to "find usable lemmas for a proof target," i.e., to dig downward along the support chain the target requires; the reverse graph is better suited for finding "which theorems use a given declaration." LeanGraphSearch uses forward dependencies, so propagation naturally unfolds along the dependency chains required by the proof, making it more likely to cover intermediate lemmas along the full proof path rather than merely recalling similar declarations at the same level as the target.

Retrieval Metrics: Recall and Full Proof Path Coverage

On mathematical retrieval benchmarks, LeanGraphSearch shows clear improvements over the strongest baseline, LeanSearch v2. On MathlibQR, recall improves by up to 12%; on MathlibMPR, its coverage of fully annotated proof paths increases, additionally covering up to 3.7% of problem groups. These two metrics show from different angles that dependency graph search can indeed recover supporting lemmas missed by semantic matching, and that these lemmas often lie on full proof paths rather than being irrelevant noise.

End-to-End Validation: Can Retrieval Gains Translate into Proving Ability?

Good retrieval metrics do not necessarily mean a stronger prover. The authors integrated LeanGraphSearch into a Lean-feedback-guided iterative proving loop and evaluated end-to-end pass rates on three theorem proving benchmarks. Results show that under {8, 16, 32} reflection rounds, LeanGraphSearch improves pass rates by up to 40% over standard provers and by up to 10% over LeanSearch v2. More importantly, the efficiency ratio between accuracy and cost is better: this means the gains do not come solely from more rounds or greater computation—part of the benefit comes from retrieval quality itself.

An implicit conclusion here is that how retrieval and proving are coupled affects the final outcome. By placing graph retrieval directly into an iterative loop signaled by Lean feedback, retrieved lemmas are repeatedly utilized as the proof state changes, allowing structural information to continue playing a role.

The Lean-feedback-guided iterative proving loop means that in each round of attempts, the prover calls the Lean kernel to check the current proof state; if it fails, it generates a new retrieval query based on error messages, unresolved goals, or remaining hypotheses, calls lemma retrieval again, and updates the proof script, repeating this process. Reflection rounds are the number of iterations of this loop, commonly set to 8, 16, or 32. Since each round produces new subgoals or proof states, the retrieval query also changes, so the retriever cannot perform only a one-time static match; it must repeatedly provide lemmas relevant to the current state within the loop. LeanGraphSearch's graph propagation results are reused multiple times in such loops, allowing structural information to continuously influence candidate selection in subsequent rounds—this is also why retrieval quality can partially translate into end-to-end pass rate improvements.

The Significance of Structure-Aware Search

LeanGraphSearch's results point to a broader research direction: proof discovery requires structure-aware search, and the dependency graph is one effective structure for it. What it reveals is not just that "retrieval can be better," but that "retrieval should be co-designed with the proving process." When the retriever understands the dependency topology between declarations, what it recalls is no longer isolated similar text, but a candidate set capable of supporting the proof chain.

For formal mathematics and AI-assisted proving, the potential value of such methods lies in scalability: the dependency graph comes from the library itself and requires no additional annotation; propagation and reranking are also relatively lightweight. Worth watching next is whether this graph retrieval can generalize to libraries beyond Mathlib, and how far it can go when combined with other structural signals, such as the abstraction levels of proof scripts.

One-line Summary

LeanGraphSearch uses Mathlib's dependency graph for multi-hop propagation retrieval, significantly improving lemma recall and end-to-end proving pass rates.

Paragraph Summary

Aiming at the blind spot in lemma retrieval for formal theorem proving, LeanGraphSearch points out that traditional semantic matching ignores multi-hop dependencies between declarations, causing supporting lemmas that are literally dissimilar yet lie on the proof path to be missed. Methodologically, it builds a forward dependency graph for Lean 4's Mathlib, first performs semantic matching to locate anchors, then uses graph ranking to propagate relevance along dependency edges, and finally reranks candidates. On MathlibQR, recall improves by up to 12% over LeanSearch v2, and on MathlibMPR it additionally covers up to 3.7% of full proof path problem groups. After integration into a Lean-feedback-guided iterative proving loop, under 8/16/32 reflection rounds, pass rates improve by up to 40% over standard provers and by up to 10% over LeanSearch v2, with better accuracy-cost efficiency. The article emphasizes that retrieval should be co-designed with the proving process, and that the dependency graph is an effective structural signal derived from the library itself without additional annotation.