LeanGraphSearch：沿依赖图搜 Mathlib，Lean 证明成功率提升 8 个百分点
kaiwei_chang · x · 2026-10-17
Jiachen Gu 等人发布 LeanGraphSearch，核心洞察是：AI 证明定理所需的引理，可能与目标定理本身「长得完全不像」——靠表面相似检索会漏掉关键材料。
- 方法：不按查询相似度，而是沿 Mathlib 中相关结果背后的形式化依赖关系图进行搜索，逐跳挖掘缺失的证明素材
- 效果：MathlibQR 召回率 94.7%（比 LeanSearch v2 的 82.7% 高 12.0pp）；MathlibMPR 覆盖率 42.8%（+3.7pp）；FATE-H 定理证明成功率 81%，比无检索的 52% 和 LeanSearch v2 的 73% 分别提升 29 和 8 个百分点，且产出更多 Lean 验证通过的证明
「编程与Agent」频道最新
- Rob Leclerc:现有 AI 编码体验仍糟糕，「胶带」撑起的表象终将被超越 — robleclerc · 2026-10-17
- AI Agents 迎来「Kubernetes 时刻」：Agent 逻辑正下沉到平台层 — bibryam · 2026-10-17
- 工程师长文分享:如何搭建一台「个人软件工厂」 — maddiehfaulkner · 2026-10-17
- 45 年资深游戏程序员:Agent 编程是我见过最大的一次生产力跃升 — IgorCarron · 2026-10-17
- 北大三星 RealtimeBench:慢模型离线指导让快模型游戏分从13.51升至24.19 — rohanpaul_ai · 2026-10-17
- Scale AI 开源 AgentEnv 框架登陆 Hugging Face,专注 RL 环境 — ben_burtenshaw · 2026-10-17