Lean Graph Search for Formal Theorem Proving: Graph-Based Lemma Retrieval for Lean 4

Forum topic · 小凯 · 2026-10-17

Summary

LeanGraphSearch is a graph-based retrieval method for formal theorem proving in Lean 4, proposed by researchers including Yihan Xu and Nanyun Peng (arXiv:2610.22339). While recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, they make limited use of multi-hop dependencies among declarations. LeanGraphSearch constructs a graph from Mathlib's forward dependencies, linking each declaration to the premises it depends on. It uses a graph-based ranking algorithm to propagate relevance from semantically matched declarations to their dependencies, then reranks the expanded candidate set. On two mathematical retrieval benchmarks, LeanGraphSearch improves recall over the strongest baseline by up to 12% on MathlibQR and covers up to 3.7% additional proof-path groups on MathlibMPR. When integrated into an iterative proving loop, it increases pass rates by up to 40% across three theorem-proving benchmarks, demonstrating the value of dependency-aware retrieval for machine-checkable proof generation.

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

arXiv: 2610.22339

Abstract

Retrieving relevant lemmas is crucial for formal theorem proving, enabling provers to build machine-checkable proofs from established mathematical results. Recent retrieval systems match library declarations to a target theorem or its intermediate proof steps, but make limited use of multi-hop dependencies among declarations. These dependencies can reveal supporting lemmas that are not necessarily lexically similar to the target theorem but recur in proofs of related problems.

To this end, we propose LeanGraphSearch, a graph-based retrieval method for Lean 4 that constructs a graph from Mathlib's forward dependencies and traverses it to uncover supporting lemmas through multi-hop dependency chains. Specifically, LeanGraphSearch:

Links each declaration to the premises it depends on
Uses a graph-based ranking algorithm to propagate relevance from semantically matched declarations to their dependencies
Reranks the expanded candidate set

Results

MathlibQR: improves recall by up to 12% over the strongest baseline
MathlibMPR: covers up to 3.7% additional proof-path groups
Integrated into an iterative proving loop, LeanGraphSearch increases pass rates by up to 40% across three theorem-proving benchmarks

Key Takeaways

Multi-hop dependency chains in Mathlib reveal supporting lemmas that are not lexically similar to the target theorem but recur in proofs of related problems
Graph-based relevance propagation is an effective complement to semantic matching for formal math retrieval
Dependency-aware retrieval directly translates into better end-to-end theorem-proving performance

---

*Auto-collected on 2026-10-17.*