LeanGraphSearch

LeanGraphSearch is a graph retrieval method for Lean 4 formal theorem proving that, by constructing a graph from Mathlib's forward dependencies, first performs semantic matching to locate anchor points, then uses a graph ranking algorithm to propagate relevance along dependency edges, and finally re-ranks the candidate set.

On the MathlibQR benchmark, LeanGraphSearch improves recall by up to 12% relative to the strongest baseline, LeanSearch v2.

On the MathlibMPR benchmark, LeanGraphSearch additionally increases coverage of fully annotated proof paths by up to 3.7% of problem groups.

In end-to-end evaluations at {8, 16, 32} reflection rounds, LeanGraphSearch improves the pass rate by up to 40% over an ordinary prover and by up to 10% over LeanSearch v2.

LeanGraphSearch uses a forward dependency graph (edges go from a declaration to the premises it references), and the propagation direction follows the decomposition direction in the proof from goal to subgoals, so as to cover the intermediate lemmas along the complete proof path.

The core judgment of LeanGraphSearch is: proof discovery is essentially a structure-aware search problem, not merely a text similarity ranking problem.

The graph ranking algorithm of LeanGraphSearch can use methods such as Personalized PageRank, random walks, or weighted propagation with decay, using the semantic matching scores as seed signals that propagate along forward dependency edges.

The dependency graph of LeanGraphSearch comes from Mathlib itself, requires no additional annotation, and its propagation and re-ranking are relatively lightweight, so it has scalability potential.

LeanGraphSearch has a better efficiency ratio of accuracy to cost in end-to-end evaluations, indicating that the pass rate improvement does not come only from more rounds or greater computation, and that part of the gain comes from retrieval quality itself.