LeanGraphSearch
for Formal Theorem Proving

Find the lemmas behind the lemmas.

Yihan XuJia-Chen GuJunyi ZhangDi WuHaikang Deng

Po-Nien KungKai-Wei ChangAmit SahaiWei WangNanyun Peng

UCLA PlusLab

Paper Code
Semantic matches lead to shared and multi-hop premises. Selected results compare LeanSearch v2 with LeanGraphSearch: MathlibQR recall 82.7 to 94.7 percent, MathlibMPR route coverage 39.1 to 42.8 percent, and FATE-H proving success 73 to 81 percent.
Semantic similarity finds a starting point. Formal dependencies reveal what supports it.
Selected results from Figure 1. MathlibQR: Recall@100; MathlibMPR: Covered@20; FATE-H: pass@32, reasoning mode with failure memory.

Beyond direct query matching

Useful premises are not always similar premises.

Formal theorem proving relies on finding the right definitions, theorems, and lemmas in a large library. A relevant declaration is often a useful starting point, but the supporting lemmas behind it may look very different from the original query.

LeanGraphSearch follows these structural connections. It builds a directed graph from Mathlib declarations to the premises they reference, starts from semantically relevant declarations, and uses personalized PageRank to uncover supporting lemmas along multi-hop dependency chains. A second reranking pass evaluates the expanded candidates against the original query.

We evaluate both premise retrieval and downstream theorem proving. The method improves declaration recall on MathlibQR and complete proof-route coverage on MathlibMPR. In an iterative Lean proving loop, graph retrieval also improves proof completion and reduces aggregate API cost per solved problem in the standard-mode configuration.

+12.0 pp

MathlibQR Recall@100
82.7% → 94.7%

+3.7 pp

MathlibMPR Covered@20
39.1% → 42.8%

From library structure to proof context

How LeanGraphSearch works

Static analysis with jixia extracts references from declaration types and values. Each edge points from a declaration to a dependency. At query time, retrieval proceeds in three stages:

Figure 2: jixia constructs a Mathlib declaration dependency graph. Semantic seed retrieval is followed by query-aware personalized PageRank, candidate merging, a second reranking, and final score fusion.
Figure 2 from the paper: dependency graph construction and graph-based retrieval.
  1. 01

    Retrieve semantic seeds

    Qwen3 embeddings retrieve candidates; a Qwen3 reranker selects declarations relevant to the query.

  2. 02

    Follow formal dependencies

    Personalized PageRank propagates relevance toward dependencies, while restarts keep the search anchored to the query.

  3. 03

    Refine the candidates

    Merge seed and graph candidates, rerank them against the query, and combine relevance with normalized graph scores.

Inside a Lean proving loop

The prover revises one proof candidate using Lean compiler feedback and retrieved premises. Optional problem-local failure memory records recurring formal states to help avoid repeated failed repairs. We compare standard and reasoning retrieval modes, with and without memory, under the same prover and reflection budgets.

Retrieval quality · Proof completion · API cost

Experimental results

Find declarations. Recover complete proof routes.

On the 810-query fair subset of MathlibQR, graph retrieval improves every reported metric. On MathlibMPR, complete-route coverage improves at every evaluated cutoff.

MathlibQR · 810 queries over 171 shared declarations · Paper Table 1
MethodnDCG@1nDCG@5nDCG@10Recall@10Recall@50Recall@100
LeanExplore0.2460.3580.3930.5690.7430.789
LeanFinder0.3700.5140.5330.6980.8240.875
LeanSearch v2 Standard0.4720.5960.6160.7650.8210.827
LeanGraphSearch Standard0.4730.6040.6290.7940.8990.947
MathlibMPR · Complete-route coverage (%) · Selected rows from Paper Table 2
MethodCovered@5Covered@10Covered@20Covered@30Covered@50
LeanSearch v2 Reasoning22.529.739.141.341.3
LeanGraphSearch Reasoning23.931.942.843.544.2

Covered@k requires every premise group in at least one annotated proof route to be retrieved. MathlibMPR rows are arithmetic means over Gemini 3.1 Pro and Claude Sonnet 5. LeanExplore and LeanFinder results are quoted in the paper from Gao et al. (2026).

Explore and reproduce

The source package includes the retrieval pipeline, graph construction, proving loop, small benchmark inputs, and experiment presets. Model weights, corpora, indexes, and graph artifacts are prepared separately using the documented dependency setup.

Read the paper Browse the code Reproduction guide