DeepMind 发布 AlphaProof Nexus：用几百美元算力，解开 56 年未解数学题

过去解决一个半个世纪没人解开的数学难题，往往需要顶尖数学家闭关数年，甚至耗尽整个学术生涯。

现在，这个周期被压缩成了几个小时，外加一张几百美元的算力账单。

Google DeepMind 正式发布 AlphaProof Nexus 论文。这个专门用于生成机器验证数学证明的 AI 系统，在一共 353 个开放数学难题中，一口气自主攻克了 9 个保罗·埃尔德什（Paul Erdős）难题，顺便还证明了《整数序列在线百科全书》（OEIS）中的 44 个未解猜想。

这 9 个关于组合数学和图论的难题里，有两个从 1970 年提出至今，已经整整 56 年无人能解。

把大模型和 Lean 焊死在一起

AlphaProof Nexus 的厉害之处，不在于它算得有多快，而在于它彻底摆脱了大模型容易「胡说八道」的毛病。

DeepMind 把大语言模型和一个叫做 Lean 的形式化证明辅助工具绑在了一起。大模型负责天马行空地给出证明思路和步骤，Lean 则扮演毫无感情的严苛裁判。

系统把步骤翻译成代码扔给 Lean，Lean 负责跑编译器级别的形式化验证。只要有一步逻辑不严密，直接打回重来；大模型根据反馈重新调整，不断循环，直到 Lean 判定完全通过。

完整版的 Agent 里甚至加入了进化算法，用来优化求解路径。DeepMind 也测试过一个更简化的版本，虽然最终也能解出同样的结果，但算力消耗和花费明显高得多。

这也把前沿数学研究的门槛拉到了一个夸张的地步：解开一个半个世纪的难题，单题推理成本只要几百美元。

刚被 OpenAI 抢了风头，隔天就反击

有意思的是这次发布的时机。

就在论文公开的前一天，OpenAI 刚刚宣布自己的 AI 推翻了一个存在 80 年的埃尔德什猜想。而在此几个月前，OpenAI 还曾因为宣称攻克 10 个新难题不严谨而被迫撤回过说法。

OpenAI 刚找回场子，DeepMind 隔天就甩出了一份更重磅的战报，而且拿出的是经受过机器形式化验证的硬核证明。

不过 AlphaProof Nexus 也不是万能的。论文坦承，那些需要凭空发明全新数学工具或全新构造的难题，目前的 AI 依然完全无能为力。

为什么重要

我们认为，AlphaProof Nexus 最大的意义，是证明了 AI 正在从「做题家」变成「研究员」。

以前大模型刷各种奥数竞赛题，本质上还是在人类画好的靶子内部打转。但面对 50 多年没人见过正确答案的开放数学猜想，AI 给出了真正的原始突破。

对数学界来说，这种工具不会砸掉数学家的饭碗，反而会成为极其强悍的研究副驾驶。人类学者负责提出宏观猜想和方向，繁琐、漫长、极度消耗脑力的构造与验证过程，完全可以打包丢给几百美元算力的 AI 去扫雷。

对行业而言，这场竞争也标志着 AI 推理的评测基准彻底换代。当模型在公开基准上全员拿满分时，去未解科学前沿实测，就成了巨头之间唯一有说服力的试金石。

DeepMind 这一步走得相当漂亮。它用 Lean 形成闭环，用确定性干掉了不确定性。虽然它现在还不能像大师那样开创全新的数学流派，但把已知世界的逻辑推演做到极致，本身就已经足够改变游戏规则了。