Lean Graph Search for Formal Theorem Proving
arXiv, 2026
LeanGraphSearch uses Mathlib's declaration dependencies to retrieve supporting lemmas for Lean 4 proofs. It starts with semantic retrieval, propagates relevance through a dependency graph, and reranks the resulting candidates. This helps uncover useful premises that are difficult to find through similarity matching alone. Experiments on two retrieval benchmarks and three theorem-proving benchmarks show improvements in lemma recall, proof completion, and accuracy relative to inference cost when graph retrieval is integrated into an iterative prover guided by Lean feedback.