知识卡片：Lean 定理证明的图搜索检索

一句话结论

LeanGraphSearch 利用 Mathlib 前向依赖关系构图并做多跳遍历，以检索支持性引理；在提升检索召回的同时，也改善了端到端定理证明的通过率与成本效率。

研究问题

形式定理证明需要检索相关引理，以便从已有数学结果构建机器可检验的证明。已有检索系统多把库声明与目标定理或其证明中间步骤做匹配，但对声明之间的多跳依赖利用有限；这些依赖可能揭示与目标定理字面不相似、却在相关问题证明中反复出现的支持性引理。

方法/产品要点

• 面向 Lean 4 的图式检索方法，基于 Mathlib 的前向依赖构建图。
• 将每个声明链接到其依赖的前提（premises）。
• 使用图排序算法，把相关性从语义匹配的声明传播到其依赖项。
• 对扩展后的候选集针对原始查询进行重排（rerank）。
• 评测覆盖两个数学检索基准（MathlibQR、MathlibMPR）与三个定理证明基准，并集成到由 Lean 反馈引导的迭代证明循环中。

主要结果

• 在 MathlibQR 上，相较最强基线 LeanSearch v2，召回率最高提升 12%。
• 在 MathlibMPR 上，完整标注证明路径的覆盖增加，最多多覆盖 3.7% 的组。
• 端到端证明：在 {8, 16, 32} 反思轮次下，相较 vanilla prover 通过率最高提升 40%；相较 LeanSearch v2 最高提升 10%，显示出更高的准确率—成本效率。

为什么重要

把检索从“字面/语义相似”扩展到“依赖结构感知”，有助于发现证明中真正起支撑作用但表面不相似的引理；并且检索增益被验证可转化为端到端证明性能提升，为结构感知的证明发现提供了方向。

局限与不确定性

• 具体实现细节（图排序算法类型、重排策略细节）待核实。
• 三个定理证明基准的具体名称与设置待核实。
• 成本效率的度量口径（如何计算成本）待核实。
• 结论主要基于论文所述基准，跨库/跨领域泛化性待核实。

可用于图书/PPT/简报的角度

• “检索不只是找相似”：依赖图多跳检索在形式证明中的价值。
• 从检索指标到端到端任务指标的转化验证范式。
• Lean 4 / Mathlib 生态中的结构感知工具链示意。

原始材料

• 标题：Lean Graph Search for Formal Theorem Proving
• 作者：Yihan Xu, Jia-Chen Gu, Junyi Zhang, Di Wu, Haikang Deng, Po-Nien Kung, Kai-Wei Chang, Amit Sahai, Wei Wang, Nanyun Peng
• 发布：2026-10-15（arXiv 2610.22339v1）
• 分类：cs.LG
• 摘要页：https://arxiv.org/abs/2610.22339v1
• PDF：https://arxiv.org/pdf/2610.22339v1