### [谷歌DeepMind用AI一口气证明9道56年数学难题，单题成本仅数百美元](https://www.willai.cc/article/814)

**Published:** 2026-05-28T10:59:55

**Author:** hiyoho

**Excerpt:** 谷歌DeepMind最近搞了个大动作——AlphaProof Nexus，一个由Gemini驱动的形式化证明框架，一口气解决了9道悬而未决的埃尔德什（Erdős）数学开放问题，其中最老的已经被卡了56年。与此同时，它还顺手证明了在线整数序列

谷歌DeepMind最近搞了个大动作——AlphaProof Nexus，一个由Gemini驱动的形式化证明框架，一口气解决了9道悬而未决的埃尔德什（Erdős）数学开放问题，其中最老的已经被卡了56年。与此同时，它还顺手证明了在线整数序列百科（OEIS）里44个未解猜想。

![Google DeepMind AlphaProof Nexus](https://storage.googleapis.com/gdm-deepmind-com-prod-public/media/original_images/nav__dm__gemini__large.svg)

AlphaProof Nexus 由 Gemini 驱动，结合 Lean 形式化验证

### 不是”AI猜答案”，而是”机器可验证的证明”

这次和以前那些”AI做数学题”的新闻不太一样。AlphaProof Nexus 的核心是把大语言模型（LLM）和 Lean 形式化验证工具绑在一起——LLM负责生成证明思路，Lean 负责严格校验每一步逻辑是否真的成立。

这样做的好处是：证明不是”看起来对”，而是”机器严格验证过对”。传统数学界对AI生成证明最大的质疑就是”你咋知道它没在胡说”，Lean 验证正好堵住了这个漏洞。

> 关键突破：单次推理成本仅数百美元，论文与代码已在 GitHub 开源（arXiv:2605.22763，CC BY-NC-ND 4.0 协议）。

### 哪些问题被解决了？

这次解决的9道 Erdős 问题横跨组合数学和图论，其中两个最引人注目的问题已经被卡了56年。完整列表在论文附录里，这里说几个有意思的：

-   **Erdős #12**：关于整数序列中等差数列密度的猜想，困扰学界超过半个世纪
-   **Erdős #125**：30年无人给出完整证明的图论问题
-   **Erdős #846**：34年悬而未决的组合数学问题
-   其余6道问题同样来自 Erdős 遗留的353道开放问题清单，这次共解决了9道
-   额外证明了 **OEIS 百科中44个序列猜想**，覆盖组合学、优化、图论、代数几何、量子光学等领域

* * *

### 和 OpenAI 的那次突破有什么区别？

就在前不久，OpenAI 宣布他们的 AI 推翻了一个有80年历史的 Erdős 猜想。两边都在做”AI+数学证明”，但路径不太一样：

OpenAI 那次更多依赖强化学习驱动的推理，而 DeepMind 这次走的是”LLM生成 + Lean 形式化验证”的路线，两种路径各有优劣。形式化验证的好处是证明可以被机器完整检查，数学界更容易接受。

> 目前 AlphaProof Nexus 还不能解决那些需要全新数学构造的问题——它强在”验证了，不是”从无到有发明了新数学”。这个界限，也是整个领域下一步要攻克的。

### 这个方向意味着什么？

以前数学家要验证一篇论文的证明是否正确，往往要花数周甚至数月。如果 AI 能快速生成”机器可验证”的证明草稿，数学研究的速度会被整个提起来。

当然，现在说”AI 取代数学家”还早得很。目前系统能处理的是”已经被明确表述出来的数学问题”，那些需要人类直觉去”发现正确的问题”的部分，AI 还差得很远。但作为一个”超级研究助手”，它已经很能打了。

* * *

📎 原文来源：[AlphaProof Nexus 论文（arXiv:2605.22763）](https://arxiv.org/abs/2605.22763) | 参考：agentupdate.ai、IT之家、知乎相关讨论

**Tags:** AI, AI技术, AI突破, DeepMind, Erdős猜想, 定理证明, 形式化验证, 数学AI

**Categories:** AI资讯

---