发生了什么
谷歌 DeepMind 的 AlphaProof Nexus 研究成果于 2026 年 10 月 12 日经同行评审正式发表于《Science》。该系统是一个面向数学研究的自动定理证明框架，以 Gemini 3.1 Pro 为底座，在形式化语言 Lean 中起草并修订证明，由 Lean 编译器逐行校验、把报错回喂给模型再修订，遇到困难子目标时还可调用专用证明工具 AlphaProof。论文共有约 20 位作者，全部 Lean 机器证明与部分自然语言证明已公开在 GitHub。
结果：从竞赛题走向科研级数学
- 在 353 个开放的埃尔德什问题中自主解出 9 个，其中两个已悬置 56 年，成功率约 2.5%。
- 证明《整数数列在线百科全书》（OEIS）492 个开放猜想中的 44 个。
- 解决一道搁置约 15 年的代数几何（希尔伯特函数对数凹性）开放问题。
- 改进凸优化中锚定梯度下降法沿用已久的理论边界——该技术恰被用于训练部分 AI 模型。
- 论文表示，即使不调用 AlphaProof，仅凭基础版智能体（商业大模型 + Lean）也能解出那 9 个埃尔德什问题，只是计算开销更高。
为什么重要
这组结果的算法结论并非首次公开——预印本最早于 2026 年 5 月 21 日上线 arXiv，本次的真正新增是「通过了同行评审」。在 AI 数学领域争议正酣的背景下，这一进展具有方法论意义：同期 OpenAI 把数百份 AI 生成的证明直接发布到 GitHub，未提交期刊评审，引发以陶哲轩（Terence Tao）等人牵头的抵制。DeepMind 选择把成果交由《Science》评审后发表，被视为把机器证明纳入学术规范的一条可选路径；同期刊发的评论文章标题即为「用于数学研究的 AI 已经到来」。论文披露，单题（尤其是困难问题）的推理成本约在数百美元量级，且系统在形式化引擎中通过编译即意味着正确性由机器保证，不存在「自说自话」的解释空间。对企业与科研机构而言，这既是自动化数学研究可行性的证据，也提示应当把「可验证性」而非「模型自称的结论」作为采用门槛。
不确定之处
其一，核心算法结果自 5 月起即为公开预印本，本次并非全新结果，窗口判定以更早的 arXiv 提交日为准。其二，2.5% 的解题率仍属低比例，全部结论均为 DeepMind 自测，尚无第三方独立复现。其三，部分数学家担忧大规模使用 AI 会削弱人类探索问题、理解证明的动力；即便 AI 未能完成证明，其尝试也可能帮助研究者发现新思路，但这一价值尚难量化。