谷歌DeepMind数学AI登上《科学》：攻克9道厄多斯难题，2题悬置56年

谷歌旗下DeepMind团队开发的数学证明AI框架AlphaProof Nexus登上最新一期《科学》杂志。该系统能自主搜索数学证明，并借助Lean等形式化工具让计算机逐步验证每一步推理是否成立。在测试中，它解决了9个此前无人攻克的厄多斯问题，其中两个已悬置超过50年。

据论文与DeepMind披露，研究团队用AlphaProof Nexus挑战了以数学家保罗·厄多斯命名的353个开放问题，系统最终攻克其中9个，两个问题的悬置时间已达56年。除此之外，它还证明了《整数数列在线百科全书》492个开放猜想中的44个，回答了代数几何中关于希尔伯特函数的开放问题，并改进了极小极大优化中的一个已知边界——后者正是训练AI模型的常用技术。

技术路线上，AlphaProof Nexus以Gemini 3.1 Pro为核心，负责在Lean形式化语言中起草并反复修改证明；Lean编译器会在每次编辑后检查证明，错误信息再反馈给模型，指导下一次尝试。遇到更难的子问题时，系统可调用专门的证明工具AlphaProof。DeepMind表示，即使不调用AlphaProof，基础版本也独立解决了上述9个厄多斯问题，论文称每个成功解出的问题仅耗费数百美元的推理成本。

这一成果的意义在于，人工智能正从解答竞赛数学题迈向探索科研级数学问题。同期评论文章认为，AI用于科研级数学的时代已经到来。也有数学家担忧，大规模使用AI可能削弱人们探索数学和理解证明的动力；DeepMind团队则认为，即便AI未能完成证明，其尝试也可能帮助数学家更好地理解问题、发现新思路。

背景上，这次发表正值AI数学争议升温。OpenAI近期将数百个AI生成的证明直接上传GitHub而非投稿期刊，由陶哲轩参与领导的“人类数学协会”呼吁数学家停止与OpenAI合作；DeepMind则选择让机器生成的证明走完同行评审，其结果经《科学》杂志审稿人检验后才公开发表，为“AI数学发现如何进入科学记录”提供了另一种范式。