先了解这件事
DeepMind开发并测试了名为AlphaProof Nexus的AI框架,相关成果于2026年10月12日公开。该框架能自主搜索数学证明,并借助Lean证明助手验证推理过程。在353个以数学家保罗·厄多斯命名的开放问题中,该系统解决了9个,其中两个已悬而未决超过50年;它还解决了《整数数列在线百科全书》492个开放猜想中的44个。团队发现,最基础版本的智能体同样解决了这9个厄多斯问题,只是处理较难问题需要更多计算资源,该版本主要依靠商业化大型语言模型和Lean证明助手。另有报道称,该系统还解决了代数几何中的一个开放问题,并改进了min-max优化中的一个已知界;其基于Gemini 3.1 Pro,用Lean起草和修订证明,遇到更难子问题时还可调用专用证明工具AlphaProof,但即使不调用也能解决那9个厄多斯问题。该研究发表在《科学》杂志并经过同行评审。
AI 根据公开报道生成
事件进展
1 个已确认进展
- 来源：The Decoder
报道与讨论时间线
按时间查看正式报道与传播讨论；两类内容的证据等级保持独立。
10月12日
The Decoder精选
Google DeepMind 的 AlphaProof Nexus 解决数十个开放数学问题并通过同行评审
Google DeepMind 的新研究显示，AlphaProof Nexus 自主解决了 353 个 Erdős 开放问题中的 9 个，其中两个已悬置 56 年，相关解法在论文发表前已公开。该系统还证明了 OEIS 整数序列数据库中的 44 个猜想，解决了代数几何中的一个开放问题，并改进了 min-max 优化中的一个已知界。它基于 Gemini 3.1 Pro，用形式化语言 Lean 起草和修订证明，Lean 在每次修改后检查草稿，错误信息引导下一次尝试；遇到更难的子问题时还可调用专用证明工具 AlphaProof，但即使不调用 AlphaProof 也能解决那 9 个 Erdős 问题。该研究发表在 Science 上，并经过了同行评审，而 OpenAI 近期将数百个 AI 证明直接发布到 GitHub 而非提交期刊，由 Terence Tao 领导的 Association for Human Mathematics 呼吁抵制。
科学网
DeepMind 的 AlphaProof Nexus 解决 9 个厄多斯问题，成果登《科学》
谷歌旗下 DeepMind 团队开发并测试了名为 AlphaProof Nexus 的 AI 框架，它能自主搜索数学证明并借助 Lean 证明助手验证推理过程，相关成果发表于《科学》杂志。在 353 个以数学家保罗·厄多斯命名的开放问题中，该系统解决了 9 个，其中两个已悬而未决超过 50 年；它还解决了《整数数列在线百科全书》492 个开放猜想中的 44 个。团队发现最基础版本的智能体同样解决了这 9 个厄多斯问题，只是处理较难问题需要更多计算资源，该版本主要依靠商业化大型语言模型和 Lean 证明助手。