LeanGraphSearch 用 Mathlib 多跳依赖图改进 premise retrieval，并把结构化检索收益传导到端到端证明

Xu 等提出 LeanGraphSearch：先从 Mathlib 的 forward dependencies 构建 declaration graph，再从语义检索得到的初始候选向其多跳依赖传播 relevance，最后重新排序供 prover 使用。论文在 MathlibQR 上报告相对最强 baseline LeanSearch v2 的 recall 最高提升 12%，在 MathlibMPR 上完整覆盖 annotated proof-route groups 的比例额外提升 3.7 个百分点；将检索器接入带 Lean feedback 的迭代 proving loop 后，在 8/16/32 轮 reflection 设置中，pass rate 相对原始 prover 最高提升 40%，相对 LeanSearch v2 最高提升 10%。公开仓库提供统一检索/证明实现、benchmark 子集和复现实验说明。