共计 1266 个字符，预计需要花费 4 分钟才能阅读完成。
谷歌 AI 框架 AlphaProof Nexus 攻克 2 道悬置 56 年数学难题
建议按 ” 变化—原因—影响 ” 的顺序阅读。
AI 正在进入更严肃的数学研究场景。 谷歌 DeepMind 最新披露的 AlphaProof Nexus, 将大语言模型生成证明与 Lean 形式化验证结合, 在多个开放数学问题中给出了可检查的证明结果, 其中包括两道悬置 56 年的 Erdős 问题。
📌 从“会推理”到“可验证”:AlphaProof Nexus 的关键变化
数学证明不同于一般问答, 结论不仅要看起来合理 , 还必须经得起逐步核验。AlphaProof Nexus 的思路, 是让大模型负责提出证明路线和证明文本, 再交由 Lean 这类形式化证明系统检查每一步是否合法。
Lean 可以把数学命题、定义和推导写成严格代码 , 由编译器判断证明是否成立。换句话说, 模型不只是“给答案”, 还需要在形式系统里通过验证, 这大幅降低了幻觉式推理带来的风险。
这类路线的核心价值在于:AI 的探索能力与形式化系统的严谨性被放在同一个循环中。
🔍 已公布结果: 多个开放问题获得证明
根据谷歌论文披露,AlphaProof Nexus 在 353 个开放的 Erdős 问题中自主解决了 9 个, 其中 2 个问题此前已悬而未决 56 年。Erdős 问题由数学家保罗·埃尔德什提出或相关, 覆盖组合数学、数论、图论、几何等多个方向。
- 在 OEIS 的 492 个开放猜想中证明了 44 个;
- 解决了 1 个存在 15 年的 Hilbert 函数问题;
- 在凸优化相关问题中改进了已有界限;
- 单个问题的推理成本被描述为数百美元级别。
💡 四级智能体架构: 从简单循环到进化搜索
AlphaProof Nexus 由 4 类复杂度递增的 AI 智能体组成。最基础的 Agent A 依靠 Gemini 3.1 Pro 与 Lean 编译器反复交互;Agent B 接入 AlphaProof, 用于补全缺失的证明片段;Agent C 加入类似 AlphaEvolve 的进化机制, 让多个证明草稿共享、评分和排序;Agent D 则整合上述能力, 形成更完整的证明搜索系统。
📊 为什么值得关注: 模型能力与编译器反馈形成闭环
这项进展的看点, 不只是“AI 解出了几道题”, 更在于方法论的变化。研究团队认为, 结果反映出两方面趋势: 底层大模型的推理和代码化表达能力持续增强; 同时, 编译器反馈正在成为约束和修正大模型推理的重要“锚点”。
- 对数学研究:AI 或可承担部分证明搜索、反例探索和形式化整理工作;
- 对大模型发展: 严谨反馈环境能帮助模型减少无效推理;
- 对科研工具:Lean 等形式化系统的重要性可能进一步上升。
🚀 行业观察:AI 数学突破仍需谨慎看待
开放问题被形式化证明并通过验证, 是值得重视的信号 。但数学研究的完整价值, 还包括问题选择、概念创造、理论统一和结果解释。AlphaProof Nexus 展示的是 AI 在可验证搜索中的能力, 而不是对人类数学工作的简单替代。
可以确定的是, 随着大模型、形式化证明语言和自动搜索框架结合得更紧密 ,AI 参与数学研究的方式会更具体, 也更容易被检验。对于科研社区而言, 这或许比一次性的“攻克难题”更具长期意义。
