Google Deepmind 的 AlphaProof Nexus 独立解决数十个未解决数学难题并获同行评审

一句话结论

Google Deepmind 的 AlphaProof Nexus 系统独立解决多个未解决数学难题，其研究成果已通过同行评审发表。

关键要点

• AlphaProof Nexus 解决了 353 个未解决的 Erdős 问题中的 9 个，其中两个问题已悬置 56 年。
• 该系统证明了 OEIS 整数序列数据库中的 44 个猜想。
• 模型解决了代数几何中的一个开放问题，并改进了最小-最大优化技术中的已知界限，该技术用于训练部分人工智能模型。
• AlphaProof Nexus 基于 Gemini 3.1 Pro 构建，使用 Lean 形式语言起草和修订证明，每次编辑后由 Lean 检查器验证，错误信息指导下一轮尝试。
• 团队在论文发表前已将这些解决方案公开共享，整个研究过程接受了正式的同行评审。

背景与事实

Google Deepmind 团队在学术期刊《科学》（Science）上发表了一项新研究，展示其人工智能系统 AlphaProof Nexus 在纯数学领域取得的具体突破。该系统并非简单生成猜测，而是通过迭代验证流程独立完成了数学证明。核心机制围绕 Gemini 3.1 Pro 大模型展开，该模型负责在 Lean 形式化语言环境中起草和修订数学证明。Lean 作为自动定理证明器，在每次模型编辑后即时检查证明草稿的逻辑正确性，并输出具体的错误信息，这些反馈直接指导模型在下一轮迭代中修正缺陷。面对更复杂的子问题，系统可以调用专用的证明工具 AlphaProof 进行辅助求解。值得注意的是，Google Deepmind 报告称，即使在没有调用 AlphaProof 辅助的情况下，AlphaProof Nexus 也独立解决了那 9 个 Erdős 问题。

除了 Erdős 问题，该系统还在其他数学分支展现出能力。它证明了 OEIS 在线整数序列百科全书中的 44 个猜想，这表明其对数论结构具有深度理解。此外，模型解决了一个代数几何领域的开放问题，并在最小-最大优化领域改进了已有的性能界限。最小-最大优化是训练某些人工智能模型（如生成对抗网络）的关键技术，这一改进可能对人工智能算法本身产生间接影响。

这项研究发表之际，人工智能在数学领域的能力正引发行业激烈争论。OpenAI 近期将其生成的数百份人工智能证明直接发布在 GitHub 代码库中，而非通过传统学术期刊渠道。由著名数学家 Terence Tao 主导的“人类数学协会”（Association for Human Mathematics）对此提出强烈反对，甚至呼吁抵制此类做法。与之形成鲜明对比的是，Google Deepmind 选择将 AlphaProof Nexus 的成果提交给《科学》期刊，接受了严格的同行评审流程。团队还在论文正式发表前，将部分解决方案在线公开，这种透明化处理旨在接受学术共同体的检验。

影响分析

对中文开发者与从业者而言，这一事件标志着人工智能辅助数学研究的范式从“生成猜想”转向“可验证证明”。AlphaProof Nexus 基于 Lean 的迭代验证机制，为构建高可靠性的形式化数学工具提供了参考架构。开发者在训练涉及复杂逻辑推理的模型时，可以借鉴这种“生成-即时验证-反馈修正”的闭环流程，而非仅依赖模型的概率输出。由于系统改进了最小-最大优化的界限，从事深度学习算法优化的工程师应关注这一理论进展，它可能为模型训练稳定性的提升提供新的数学基础。同时，Google Deepmind 通过同行评审发布结果的做法，为人工智能数学成果的学术规范化树立了标杆，开发者在发布相关研究成果时应重视合规性与可复现性。

适用边界

该结论仅适用于涉及形式化语言（如 Lean）支持、且具备即时自动验证机制的数学证明场景。对于高度依赖直觉、缺乏形式化定义或非良构的纯数学探索，AlphaProof Nexus 的方法可能不适用。此外，该系统针对的是离散数学、数论及特定代数几何问题，其在连续动力系统或拓扑学等其他数学分支的表现尚未在此研究中明确验证。同行评审仅针对《科学》期刊发表的特定研究内容，不代表所有人工智能生成的数学结论均具备同等学术认可度。

孤本观察

AlphaProof Nexus 通过同行评审这一动作，实质上在人工智能数学能力争议中划定了“可接受证据”的边界。编辑判断认为，这种将形式化验证与学术规范结合的模式，比单纯堆砌 GitHub 上的未验证证明更具长期学术价值。

来源：The Decoder