LEAN GRAPH SEARCH FOR FORMAL THEOREM PROVING

Authors: Yihan Xu, Jia-Chen Gu, Junyi Zhang, Di Wu, Haikang Deng, Po-Nien Kung, Kai-Wei Chang, Amit Sahai, Wei Wang, Nanyun Peng

Affiliation: University of California, Los Angeles

---

Summary (Overview)

• Novel graph-based retrieval framework: The paper introduces LEANGRAPHSEARCH, a retrieval method for Lean 4 theorem proving that constructs a directed dependency graph from Mathlib's formal declarations and uses personalized PageRank (PPR) to propagate relevance along multi-hop dependency chains, enabling discovery of supporting lemmas that are not lexically similar to the query.

• Significant retrieval improvements: LEANGRAPHSEARCH improves Recall@100 from 82.7% (LeanSearch v2) to 94.7% on the MathlibQR benchmark (+12 percentage points) and increases complete annotated proof-route coverage (Covered@20) from 39.1% to 42.8% on MathlibMPR (+3.7 percentage points).

• End-to-end proving gains: When integrated into an iterative proving loop with Lean feedback, LEANGRAPHSEARCH improves pass rates at {8, 16, 32} reflection turns by up to 40% compared to the vanilla prover and up to 10% compared to LeanSearch v2, achieving a better accuracy–cost tradeoff.

• Cost efficiency: LEANGRAPHSEARCH in Standard Mode achieves the lowest API cost per solved problem, while Reasoning Mode with failure memory achieves the highest aggregate completion (151 of 210 problems solved).

• Failure memory innovation: The paper introduces a problem-local failure memory mechanism that records recurrent formal proof states via SHA-256 hashing, preventing the prover from repeating identical failed attempts and improving performance under limited reflection budgets.

---

Introduction and Theoretical Foundation

Background

Formal theorem proving expresses mathematical statements and proofs in a formal language, allowing proof assistants like Lean to verify correctness (de Moura & Ullrich, 2021). Search engines support this process by helping users and automated provers locate useful definitions, theorems, and lemmas within large mathematical libraries such as Mathlib (The mathlib Community, 2020; Yang et al., 2023; Mikuła et al., 2024; Shen et al., 2025; Ju et al., 2026).

Motivation

Existing retrieval systems (LeanExplore, LeanFinder, LeanSearch v2) identify library declarations relevant to a target theorem or intermediate goal but make limited use of multi-hop dependencies among declarations. This limitation may cause them to miss supporting lemmas that:

• Share little lexical similarity with the query
• Occur in proofs of related problems
• Are connected through formal dependency chains

Key Insight

Declarations relevant to a target theorem can serve as starting points for discovering supporting lemmas through multi-hop dependencies. These dependencies connect declarations to their direct and indirect premises, providing extra paths to useful lemmas that are less lexically similar to the query.

Theoretical Foundation

The approach builds on personalized PageRank (PPR) (Brin & Page, 1998), which propagates relevance scores along graph edges while periodically restarting from a seed distribution. This is adapted to the formal dependency graph of Mathlib, where edges point from declarations to their formal prerequisites.

---

Methodology

3.1 Task Formulation

Mathematical Retrieval: Let $\mathcal{L} = \{d_i\}_{i=1}^{n}$ denote the Mathlib declaration corpus. Each declaration $d_i$ is identified by its name, formal statement, and (when available) natural-language description. Given a query $q$ (informal description, formal Lean statement, proof state, or combination), the retriever returns up to $K$ declarations ranked by retrieval score: $\mathcal{R}(q) = \{d_j\}_{j=1}^{\hat{K}}$.

Theorem Proving: Each problem is specified by a Lean source $x$ with one target proof hole. At round $t$, the prover generates a candidate $Y_t$ conditioned on the problem, preceding candidate, Lean diagnostic, retrieved declarations, and failure memory.

3.2 Declaration Dependency Graph Construction

LEANGRAPHSEARCH constructs a directed graph $G = (V, E)$ from structural references in Mathlib using static analysis with the jixia tool (frenzymath, 2024):

• Each node $i \in V$ represents one declaration with its formal statement and description
• A directed edge $i \rightarrow j$ indicates declaration $i$ references declaration $j$ in its type or value
• Edges point from declarations to their dependencies, enabling traversal from query-relevant declarations to underlying definitions and lemmas

3.3 Graph-Based Retrieval

The retrieval pipeline consists of three stages:

Stage 1: Semantic Seed Retrieval

The query $q$ is encoded with Qwen3-Embedding-8B (Zhang et al., 2025) to retrieve an initial candidate set. Each query–declaration pair is then scored using Qwen3-Reranker-8B logits. The top $K$ declarations form the semantic seed set $S$.

Stage 2: Query-Personalized Propagation

The semantic seed scores are normalized to form a seed distribution $v$ over graph nodes:

$$v_i = \frac{q_i \cdot \mathbb{1}[i \in S]}{\sum_{j \in S} q_j} \tag{1}$$

Let $P$ denote the row-stochastic transition matrix of $\mathcal{G}$ and $\mathcal{D}$ the set of dangling nodes. Personalized PageRank is computed by iterating:

$$p^{(k+1)} = r v + (1 - r) p^{(k)} P + (1 - r) \left(\sum_{i \in \mathcal{D}} p_i^{(k)}\right) v \tag{2}$$

where $p^{(0)} = v$. The restart term $rv$ keeps propagation anchored to the seed distribution, while the transition term $(1-r)p^{(k)}P$ expands each seed toward its dependencies. Dangling mass is returned to $v$ to preserve the query-specific distribution.

Stage 3: Graph-Aware Candidate Refinement

The semantic seed set $S$ is merged with the top-$N$ graph-expanded candidates ranked by PPR score. All retained candidates are scored against the original query via the reranker. The final score mixes the second-stage relevance score $\tilde{q}_i$ with the normalized PPR score weighted by coefficient $\lambda$:

$$f_i = \tilde{q}_i + \lambda \, \mathrm{zscore}_{\mathrm{query}}(p_i) \tag{3}$$

The top-$K$ candidates with highest $f_i$ form the final retrieval $\mathcal{R}(q)$.

3.4 Search Loop Policy

Two retrieval-policy variants are evaluated:

• Standard Mode: Invokes graph-based retrieval after a failed proof attempt using queries conditioned on the current proof state
• Reasoning Mode: Uses an LLM to decompose the theorem into subqueries targeting definitions, proof strategies, and individual proof steps before the first proof attempt

Agentic Proving Loop with Failure Memory

The prover generates candidates according to:

$$Y_t \sim M_\theta(x, Y_{t-1}, e_{t-1}, R_t, m_{t-1}) \tag{4}$$

where $x$ is the problem, $Y_{t-1}$ the preceding candidate, $e_{t-1}$ the Lean diagnostic, $R_t$ retrieved declarations, and $m_{t-1}$ failure-memory feedback.

Failure memory records structured failure states:

$$s_t = (c_t, \bar{e}_t, G_t, L_t, \tau_t) \tag{5}$$

where $c_t$ is the error category, $\bar{e}_t$ the normalized diagnostic, $G_t$ unresolved goals, $L_t$ the local context summary, and $\tau_t$ the inferred failing tactic. A deterministic serialization and SHA-256 (NIST, 2015) hash identify repeated states, preventing the prover from repeating identical failed attempts.

---

Empirical Validation / Results

4.1 Mathematical Retrieval Results

MathlibQR (810-query fair subset):

Table 1: Query-to-declaration retrieval on MathlibQR. Best results in bold.

Key gains: Recall@50 improves by 7.8 percentage points and Recall@100 by 12.0 percentage points over LeanSearch v2.

MathlibMPR (Global premise retrieval):

Table 2 (excerpt): Global premise retrieval on MathlibMPR. Results are arithmetic means over Gemini 3.1 Pro and Claude Sonnet 5.

Key gains: Covered@20 improves by 3.7 percentage points and Covered@50 by 2.9 percentage points.

4.2 Theorem Proving Results

FATE-H (100 graduate-level algebra problems, failure memory enabled):

Table 3 (excerpt): Proving results on FATE-H with failure memory enabled.

Key findings:

• LEANGRAPHSEARCH (Reasoning Mode + memory) solves 81/100 FATE-H problems, exceeding LeanSearch v2's 73 by 8 problems
• At pass@16, LEANGRAPHSEARCH solves 75 problems, surpassing LeanSearch v2's pass@32 count of 73

Aggregate results across all 210 problems (FATE-H + MathlibMPR-Prop + Lean-IMO-Bench):

• LEANGRAPHSEARCH in Reasoning Mode with memory achieves the highest aggregate completion: 151 of 210 problems solved
• LEANGRAPHSEARCH in Standard Mode achieves the lowest cost per solved problem
• At pass@8 with memory enabled, LEANGRAPHSEARCH Standard Mode increases solved problems from 106 to 111 (vs. LeanSearch v2's 99 to 105)

5.3 Qualitative Findings

1. Graph-aware expansion reveals underlying mathematical objects: Semantic retrievers often identify constructors, projections, or characteristic theorems matching the query but miss parent declarations or deeper dependent declarations. Graph-aware expansion connects these matches through dependency relationships.

2. Graph augmentation improves retrieved context composition: LEANGRAPHSEARCH returns fewer filtered declarations on average than LeanSearch v2 yet retrieves more gold declarations in the top five positions, concentrating relevant premises rather than merely expanding the context.

---

Theoretical and Practical Implications

Theoretical Contributions

1. Formal dependencies as retrieval signal: The paper demonstrates that the dependency structure recorded in a formal library provides useful guidance for retrieving supporting premises, connecting semantic search to the mathematical ingredients needed for formal proofs.

2. Multi-hop reasoning in formal mathematics: The work validates that multi-hop dependency chains reveal supporting lemmas that direct lexical/semantic matching misses, extending insights from graph-based retrieval in NLP (GraphRAG, HippoRAG) to formal mathematics.

3. Retrieval–proving connection: The paper provides strong evidence that improvements in premise retrieval quality translate directly into higher formal proof success rates, validating the importance of retrieval research for theorem proving.

Practical Implications

1. Better accuracy–cost tradeoff: LEANGRAPHSEARCH improves proof completion while maintaining or reducing API costs, making it practical for real-world deployment.

2. Failure memory as a general technique: The problem-local failure memory mechanism is a lightweight, general intervention that improves performance under limited reflection budgets and could benefit other agentic reasoning systems.

3. Structure-aware search: The results motivate further research on structure-aware search methods for proof discovery, suggesting that combining semantic and structural signals is a promising direction.

---

Conclusion

LEANGRAPHSEARCH introduces a graph-based retrieval method that exploits formal dependencies in Mathlib to discover supporting premises for Lean 4 theorem proving. The approach:

1. Constructs a directed dependency graph from Mathlib's declarations
2. Propagates relevance from semantically matched declarations along dependency edges using personalized PageRank
3. Reranks expanded candidates against the original query

Key results:

• Improvements in declaration recall (up to +12 percentage points on MathlibQR) and annotated proof-route coverage (up to +3.7 percentage points on MathlibMPR)
• Consistent improvements in downstream proof construction across FATE-H, MathlibMPR-Prop, and Lean-IMO-Bench
• Reduced aggregate API cost per solved problem

Future directions: The findings highlight the value of dependency graph search for theorem proving and motivate further research on structure-aware search for proof discovery, including potentially richer graph structures, learned graph representations, and tighter integration between retrieval and proof search policies.