# Lean Graph Search for Formal Theorem Proving

> LEANGRAPHSEARCH uses personalized PageRank over Mathlib's formal dependency graph to boost premise retrieval recall by 12 points and improve Lean 4 proof completion by up to 40%.

- **Source:** [arXiv](https://arxiv.org/abs/2610.22339)
- **Published:** 2026-10-17
- **Permalink:** https://picx.dev/p/CTx69q
- **Whiteboard:** https://picx.dev/p/CTx69q/image

## Summary

# 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):**

| Method | nDCG@1 | nDCG@5 | nDCG@10 | Recall@10 | Recall@50 | Recall@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) | 0.472 | 0.596 | 0.616 | 0.765 | 0.821 | 0.827 |
| **LEANGRAPHSEARCH (standard)** | **0.473** | **0.604** | **0.629** | **0.794** | **0.899** | **0.947** |

*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):**

| Method | Recall@20 (group) | Recall@50 (group) | Covered@20 | Covered@50 |
|--------|-------------------|-------------------|------------|------------|
| DIVER | 46.6 | 55.0 | 29.0 | 37.7 |
| LeanSearch v2 (reasoning) | 55.5 | 58.2 | 39.1 | 41.3 |
| **LEANGRAPHSEARCH (reasoning)** | **56.8** | **58.3** | **42.8** | **44.2** |

*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):**

| Retrieval condition | pass@8 | pass@16 | pass@32 | Relative cost |
|---------------------|--------|---------|---------|---------------|
| No retrieval | 33 | 45 | 52 | 1.00× |
| LeanSearch v2 (standard) | 53 | 63 | 71 | 1.01× |
| LEANGRAPHSEARCH (standard) | 54 | 68 | 73 | 1.01× |
| LeanSearch v2 (reasoning) | 54 | 66 | 73 | 1.31× |
| **LEANGRAPHSEARCH (reasoning)** | **58** | **75** | **81** | 1.22× |

*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.

---

_Markdown view of https://picx.dev/p/CTx69q, served by PicX — AI-generated visual whiteboard summaries of research papers._