LeanGraphSearch: Using Mathlib's Dependency Graph to Find the Lemmas a Lean 4 Prover Needs

Formal theorem proving has a retrieval problem. A Lean 4 prover that wants to prove a statement must find the right lemmas among hundreds of thousands in Mathlib, and the lemma it needs is often not the one whose name or docstring looks like the goal. LeanGraphSearch, from a team that includes Kai-Wei Chang and Nanyun Peng, attacks this with the library's own structure: follow the dependency links. The paper on arXiv is accompanied by public code in the PlusLabNLP/LeanGraphSearch repository.

This is a research-grade release with modest star count and honest caveats, but it speaks to a live area: AI systems are increasingly producing formal proofs, as in our coverage of Claude's Lean proof work and the collapse in the cost of Lean 4 formal proofs. Retrieval is one of the places where gains are cheap compared with training a bigger prover.

TL;DR

Why is premise retrieval hard?

A proof in Lean is built from earlier results. When you ask a language model to prove a theorem, it needs to know which prior declarations to invoke. Standard retrieval embeds the theorem statement and finds declarations that look similar in meaning or wording. That works when the needed lemma is a near match. It fails when the proof depends on a supporting lemma that has a very different statement, for instance a technical fact about filters that is needed to apply a general theorem to a concrete case.

Mathlib has a natural source of help: every declaration depends on other declarations. Those dependency links record, in the library's own structure, which results are used together. LeanGraphSearch exploits that.

How does LeanGraphSearch work?

According to the abstract and README:

1. Build a graph. Nodes are Mathlib declarations; edges are forward dependencies, so a declaration links to the premises it relies on.
2. Seed with semantic matches. An ordinary embedding search finds declarations that match the query.
3. Propagate relevance. Relevance spreads along the links, so lemmas reachable by multi-hop dependency chains get credit even if they do not resemble the target wording.
4. Rerank. The expanded candidate set is reranked against the original query, to keep the list focused.
5. Plug into a prover. The authors test whether better retrieval improves end-to-end proving by feeding results into an iterative prover that uses Lean feedback.

The name leansearchv2 stays in the code for compatibility with the upstream baseline. This is a sensible design: the graph step adds recall, and the rerank step restores precision.

What does this look like in practice?

Imagine a prover asked to show that a certain sequence of real numbers converges. A text-similarity search will happily return the convergence theorems whose statements mention sequences and limits. But the actual proof may need a result about monotone bounded sets, or an inequality lemma that never mentions convergence. Those lemmas sit nearby in the dependency graph: the convergence theorems depend on them, and so do similar proofs.

Graph propagation turns that structural neighborhood into a retrieval signal. A declaration matched by the query passes some relevance to what it depends on, and the passed relevance accumulates on lemmas that several matched declarations share. A lemma that no embedding would pick for this query can end up near the top because many relevant results lean on it. The reranker then checks the enlarged set against the actual query so a popular but irrelevant lemma does not crowd out the right ones.

This is the same intuition behind link analysis in web search, applied to a mathematical library. It is also why the authors evaluate coverage of complete annotated proof routes on MathlibMPR, not just whether a single relevant lemma appears: a proof needs the whole chain, and a retriever that finds three of four required lemmas still leaves the prover stuck.

What are people likely to ask?

Does this replace LeanSearch? No. The README keeps the upstream leansearchv2 import name for compatibility, and the paper's best comparison is against LeanSearch v2. LeanGraphSearch builds on a semantic retriever and adds graph expansion plus reranking.

Why is the gain over the best baseline in proving only up to 10 percent? End-to-end proving depends on more than retrieval. The prover has to choose among retrieved lemmas, write correct tactics and recover from Lean errors. Better retrieval removes one failure cause but not the others, so the improvement shrinks as the baseline gets stronger.

Is the method specific to Mathlib? The released code is, but the design needs only a corpus with explicit dependency edges, which many code and documentation collections have.

Who is this for? Researchers building Lean provers, teams evaluating formal-math agents, and developers of retrieval systems for structured corpora. It is not a tool for casual users.

What did the experiments show?

The README lists the benchmarks and models:

The paper's headline numbers, from the arXiv abstract page:

• Retrieval recall: up to 12 percent better on MathlibQR than the strongest baseline, LeanSearch v2.
• Proof routes: more complete annotated proof routes are covered on MathlibMPR, up to 3.7 percent extra groups.
• Proving: pass rates at 8, 16 and 32 reflection turns improve by up to 40 percent over a vanilla prover, but by at most 10 percent over LeanSearch v2, across three benchmarks. The authors describe this as better accuracy-cost efficiency.

Read the third bullet carefully. The 40 percent figure compares against a prover with no strong retrieval. The fairer comparison, against the best prior retriever, shows a smaller gain of up to 10 percent. Both are useful, but they answer different questions.

What should you be cautious about?

• Replication status. The README says no full model-based experiment was rerun when the supplement was prepared, so the numbers come from the paper, not from a fresh run of the released code.
• Small benchmarks. MathlibMPR has 69 problems and MathlibMPR-Prop 50; small changes in solved counts move percentages a lot.
• Closed models in the loop. Proving experiments use Gemini 3.1 Pro and, for retrieval, Claude Sonnet 5. Anyone reproducing the results needs access to those models and a Lean toolchain with a GPU.
• Relative gains. "Up to" figures report the best case across settings, not the average.
• Early repo. The repository had 0 stars, 0 forks and 0 watchers when we checked, and licensing is spread across three files (Apache-2.0, MIT and a PlusLab license), so check terms before reuse.

How to try it

From the README:

1. Create a Python 3.11 virtual environment and install requirements-test.txt.
2. Set PYTHONPATH to the src directory.
3. Run scripts/smoke_graph.py and the pytest suite. These need no GPU or credentials and confirm the graph code works.
4. For the full experiments, follow REPRODUCING.md: you need external models and indexes, a Lean toolchain, a GPU and model access.

If you only want the idea, you can adapt it. Any library with explicit dependencies, such as a package ecosystem or a codebase call graph, can use the same pattern: seed with semantic search, propagate along dependency edges, rerank. That is a general technique for code and documentation retrieval, not specific to Lean.

Why does this matter beyond Lean?

AI-for-math has moved from competition problems to research-level results, which we have followed in coverage of OpenAI's Lean RL environments for math, AlphaProof Nexus and Erdos problems and Meta's Muse Spark on open math problems. In formal settings, a proof is checked by the Lean kernel, so retrieval quality translates directly into proofs that either compile or do not. That makes retrieval research unusually measurable.

For general builders, the lesson is about retrieval design. Semantic similarity is a weak proxy for usefulness when the thing you need is structurally related rather than textually related. If your corpus has links, whether citations, imports or dependencies, using them can beat a bigger embedding model.

What we still do not know

• Whether the gains hold when the underlying prover and judge models change.
• How much of the improvement comes from graph propagation versus the reranker.
• How the method scales to Mathlib as it grows, and the cost of building the graph.
• Independent reproductions of the end-to-end proving numbers.

Related reading

• Claude and a Fermat's Last Theorem Lean proof
• Lean 4 formal proof cost collapse
• OpenAI math Lean RL environments on Hugging Face
• AlphaProof Nexus and peer-reviewed Erdos problems
• Meta Muse Spark on six open math problems
• Boris Cherny on Opus 5.5, Lean and TLA formal verification

Based on the LeanGraphSearch paper abstract and repository README as of October 16, 2026; figures are the authors' and unreplicated.