DeepMind AlphaProof Nexus 解出 9 个埃尔德什问题，登上 Science
DeepMind 的 AlphaProof Nexus 解出 9 个埃尔德什开放问题、44 条 OEIS 猜想，经同行评审登上 Science。
Google DeepMind 的 AI 证明系统 AlphaProof Nexus 10 月 8 日登上《Science》，论文题为 Advancing mathematics research with AI-driven formal proof search（第 394 卷第 6820 期，234–239 页）。论文记录这套系统自主解出 353 个开放埃尔德什问题中的 9 个——其中 2 个已经悬置 56 年——并证明了 OEIS 数列百科 492 条开放猜想中的 44 条。它用 Gemini 3.1 Pro 起草证明，每写一步就交给 Lean 编译器核对，报错信息反喂给模型改下一版。
要点
- 结果：9/353 个开放埃尔德什问题、44/492 条 OEIS 猜想，2026 年 10 月 8 日刊于《Science》第 394 卷第 6820 期。
- 最简配置同样有效：只用商用大模型加 Lean 循环的基础版智能体——不调用 DeepMind 专用的 AlphaProof 证明工具——也解出了全部 9 题，代价是最难题上花费更多算力。
- 全部可查：Lean 证明与配套的自然语言证明开源于 google-deepmind/alphaproof-nexus-results 仓库（Apache-2.0 与 CC-BY 4.0），预印本口径每个问题的推理成本只要数百美元。
背景
埃尔德什问题是匈牙利数学家保罗·埃尔德什留下的猜想清单，覆盖组合数学、数论、图论与几何，erdosproblems.com 逐条登记；OEIS 是整数数列在线百科，同样囤积着大量没人证明得了的猜想。
这批结果本身并不新鲜：2026 年 5 月 21 日的 arXiv 预印本（arXiv:2605.22763）已经给出 9/353 和 44/492 这两个数字，IT之家 5 月 26 日也报道过系统的四层架构。10 月 8 日真正的增量是学术承认——同一批结果通过了《Science》的同行评审，而证明本身在此前已先行公开。
同期正好有一个对照：OpenAI 10 月 6 日把 722 份 AI 数学手稿直接开源到 GitHub，没有走期刊评审，IAS 顾问组此前还公开要求它停止这类测试（见本站报道：OpenAI 公开 722 篇 AI 数学论文）。同一个星期，两条路线各走各的。
事实部分
论文与预印本给出的可核对数字如下。
| 指标 | 数字 | 出处 |
|---|---|---|
| 埃尔德什问题 | 尝试 353 个，解出 9 个 | 论文摘要（Crossref 元数据核实） |
| 悬置最久的两个 | 56 年 | The Decoder、IT之家 |
| OEIS 猜想 | 尝试 492 条，证明 44 条 | 论文摘要 |
| 其他结果 | 1 个悬置 15 年的 Hilbert 函数问题；凸优化已知界限改进 | IT之家（预印本转述） |
| 推理成本 | 每题约数百美元 | 预印本摘要 |
| 刊物 | Science 第 394 卷第 6820 期，234–239 页，2026-10-08 | Crossref |
系统的工作方式是一个循环：Gemini 3.1 Pro 用形式化语言 Lean 起草证明，编译器逐步核对每步推理是否符合公理与规则，出错就把报错交回模型，如此反复。预印本按能力递增排了四层：Agent A 只有模型加编译器；Agent B 接入 DeepMind 的专用证明工具 AlphaProof 补全缺口；Agent C 再加类似 AlphaEvolve 的进化机制，让多份草稿共享、评分、排序；Agent D 全都要。团队原本指望最复杂的 Agent D 才啃得动埃尔德什问题，结果最简单的 Agent A 也全部解出，只是在最难题上花掉更多算力。论文摘要把这点写成原话：Even a basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes.
按论文摘要的说法，这套系统已经部署进组合数学、优化、图论、代数几何和量子光学的科研流程。
各方说法
《Science》同期配发的评论给这件事定了调：AI 用于科研级数学的时代已经到来（据科技日报）。
担忧也写在同一篇报道里。科技日报引述部分数学家的意见：大规模用 AI 做数学会削弱人们探索问题、理解证明的动力。团队的回应是，即便 AI 证明失败，它的尝试也能帮数学家更好地理解问题、找到新思路。
The Decoder 把这篇论文和 OpenAI 的发布放在一句话里对照：DeepMind put its work through peer review。OpenAI 那边引发的学界反弹，由《纽约时报》等媒体跟进报道过（同见本站 10 月 7 日报道）。
怎么试
结果仓库是 github.com/google-deepmind/alphaproof-nexus-results。想核对证明，按 README 的两条命令来：
lake exe cache get
lake build
仓库只收成功案例——README 原话是 contains only problems where successful proofs were discovered。完整的尝试清单在 erdos_problems_attempted.txt，未解问题的形式化放在同组织的 formal-conjectures 仓库。自然语言证明按 CC-BY 4.0 许可，可以直接引用。
编辑判断
对做智能体的开发者，这篇论文最值得细读的是摘要里的一个词 replicated：把确定性验证器放进循环，通用大模型就够用；四层架构里的进化机制和专用工具，反而没被证明是必要的。反馈信号越硬，智能体越稳——这个经验在写代码的智能体上是相通的。
诚实的一面也要说：9/353 的通过率不到 3%；仓库只收成功证明，失败数据要去另一个仓库找；数字 5 月就公开了，这次的增量是学术承认，不是新突破。还有一点论文没给细节：评审对 Lean 证明实际核查到什么程度。这会影响「经过同行评审的 AI 证明」这句话的分量，值得继续盯。