LeanGraphSearch：基于依赖图的 Lean 4 定理证明检索方法
Lean Graph Search for Formal Theorem Proving
做了个把 Mathlib 依赖关系建成图来搜引理的工具，召回率比 LeanSearch v2 高 12%，做形式化证明的可以试试。
LeanGraphSearch 是一个面向 Lean 4 的图检索方法，从 Mathlib 的前向依赖构建图，通过多跳依赖链发现词面上不相似但有用的支撑引理。它在 MathlibQR 基准上比最强基线 LeanSearch v2 的召回率最高提升 12%，在 MathlibMPR 上额外覆盖 3.7% 的完整注解证明路径。接入基于 Lean 反馈的迭代证明循环后，在 8、16、32 轮反射设置下，相比 vanilla prover 的通过率最高提升 40%，相比 LeanSearch v2 提升最多 10%。
Lean Graph Search for Formal Theorem Proving
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, and reranks the expanded candidates against the original query. Across two mathematical retrieval benchmarks, LeanGraphSearch improves recall by up to 12% over the strongest baseline, LeanSearch v2, on MathlibQR and increases coverage of complete annotated proof routes on MathlibMPR, covering up to 3.7% of extra groups. More importantly, we evaluate whether these retrieval gains translate into improved end-to-end theorem proving by integrating LeanGraphSearch into an iterative proving loop guided by Lean feedback. Across three theorem proving benchmarks, LeanGraphSearch improves pass rate at {8, 16, 32} reflection turns by as much as 40% compared to vanilla prover and at most 10% compared to LeanSearch v2, showing higher accuracy-cost efficiency. These findings highlight the value of dependency graph search for theorem proving and motivate further research on structure-aware search for proof discovery.