LeanGraphSearch uses library dependencies to guide AI proof search
An October preprint tests whether following Mathlib’s dependency graph can help an AI prover find the supporting lemmas it needs.
Searching through the structure of a formal library
A formal proof assistant can check a finished proof, but an AI system must still locate the definitions and lemmas that make a proof possible. A preprint submitted on October 15 introduces LeanGraphSearch, a retrieval method that uses the dependency structure of the Lean 4 mathematics library Mathlib to expand the list of facts offered to a proof-generating model.
From similar words to supporting prerequisites
The method starts with ordinary semantic search: it retrieves declarations whose statements resemble a target theorem or proof state. It then follows the directed links from those declarations to the earlier facts they depend on, using a query-specific PageRank-style score. A second reranking step compares the expanded candidates with the original query. The goal is to find useful prerequisites even when their wording is unlike the problem the model is trying to prove.
The authors evaluate the approach on two retrieval benchmarks and three Lean theorem-proving benchmarks. They report higher Recall@100 than LeanSearch v2 on a selected MathlibQR subset, and better proof-completion rates than their vanilla prover at several reflection budgets. Against LeanSearch v2, their reported proof gains are smaller. The paper also combines retrieval with Lean compiler feedback and a problem-local record of earlier failed attempts.
A tool for formal proof workflows, not a new theorem
This work concerns the infrastructure around formal mathematics: how an AI system retrieves existing, machine-readable knowledge before writing a proof. Lean’s checker can validate a completed formal script, but benchmark improvements do not by themselves show that a system can independently solve open research questions. The results are the authors’ reports for their chosen datasets, models, budgets and baselines. This is an unreviewed preprint, and MathsAI has not reproduced the experiments.