AI 精选动态
智能评分 75
Advancing Mathematics Research with AI-Driven Formal Proof Search
AI 推荐理由
值得点开原文看 AlphaProof Nexus 如何把 LLM 搜索、证明助手和 Lean 验证闭环结合起来，以及它在真实开放数学题上的失败模式。核心解读
Google DeepMind 发表论文《Advancing Mathematics Research with AI-Driven Formal Proof Search》，提出 AlphaProof Nexus：让 LLM 在 Lean 形式化证明环境中反复编辑证明、读取编译错误并继续搜索，部分子问题还可调用更强的证明工具。论文在 353 个已形式化的 Erdős 问题和 492 个来自 OEIS 的开放猜想上测试，最佳 agent 解决了 9 个 Erdős 问题，并证明了 44 个序列猜想，同时还在优化、图论、代数几何和量子光学等问题上提供帮助。作者强调，验证器是核心机制：它让模型必须把“看起来合理”的证明草图转成可执行逻辑，否则会被迅速识别出错误。