AREX Feed Article
Google DeepMind 的 AlphaProof Nexus 成果通过同行评审：9 个埃尔德什问题、44 个 OEIS 猜想登上 Science
据 ，Google DeepMind 的 AlphaProof Nexus 系统解出的数学成果已通过同行评审，发表在 10 月 8 日出版的《Science》上：在 353 个开放埃尔德什（Erdős）问题中解出 9 个，其中两个已经悬置 56 年；另证明整数数列线上百科 OEIS（On-Line Encyclopedia of Integer Sequences）492 个猜想中的 44 个。这批解法今年 5 月已先行在网上公开，比正式发表早了四个多月。
论文还报告了另外两项结果：解决一个代数几何开放问题，并改进 min-max 优化的一个已知界——min-max 优化是训练部分 AI 模型时用到的一类技术。发表时机恰逢 AI 数学成果如何进入学术记录的争论：OpenAI 在 10 月 7 日把 372 份 AI 生成的数学结果直接放上 GitHub 而非投给期刊，引发人类数学协会（Association for Human Mathematics，AHM）的抵制呼吁；DeepMind 这次把工作送进了期刊评审。
5 月先行公开，10 月通过评审：论文收录了哪些结果
这篇论文题为 ，刊登于《Science》第 394 卷第 6820 期第 234～239 页。显示，论文 2026 年 10 月 8 日见刊，21 位作者中 19 人来自 Google DeepMind 伦敦，其余两人分别来自奥胡斯大学数学系和 Google 山景城办公室，第一作者是 George Tsoukalas。
论文摘要称，这些结果由一个执行形式证明搜索的 AI agent（智能体）自主完成，并称这是该方法「在规模上解决开放问题的价值」的首次演示；系统现已被部署到组合数学、优化、图论、代数几何与量子光学的在研研究中。摘要还写道，即使最基础的 agent 在大语言模型（LLM）生成与形式化证明语言 Lean 校验之间交替，也复现了埃尔德什问题上的全部成功。
解法先于论文出现在网上：the-decoder 就报道过同一批结果，当时 上，与研究论文一同公开。
系统怎么工作：Gemini 3.1 Pro 起草，Lean 编译器逐步把关
AlphaProof Nexus 以 Gemini 3.1 Pro 为核心。据 the-decoder 报道，模型在 Lean 中起草证明并逐处修改，每改一步，Lean 编译器就完整校验一次，报错信息直接进入下一轮尝试。语言模型因此不必独自撑住整条逻辑链——符号化的编译反馈为它的推理提供了安全网，人类只在最后检查结果。
系统有四种由简到繁的 agent 变体。最简单的 A 由独立子 agent 在 Gemini 3.1 Pro 上循环「生成—校验—反馈」；B 增加对 AlphaProof 的调用，那是 Google 基于强化学习、面向奥数数学的证明系统，可以补全缺失的证明步骤；C 借鉴 AlphaEvolve 加入进化机制，子 agent 共享一个证明草稿种群，由基于 Gemini 3.0 Flash 的评分 agent 按合理性与新颖度打分、用 Elo 排名；D 集齐全部能力。解埃尔德什问题时用的是 D。事后分析给出了一个意外结果：只用 LLM 加编译器反馈的 A 同样证出了全部 9 个埃尔德什问题，只是在最难的题目上花费更高。Google DeepMind 也对外报告了这一点：即使不调用 AlphaProof，系统照样解出了这 9 个问题。
成本方面，据 the-decoder 德语版援引论文，每个问题的推理成本为几百美元。
2.5% 的解题率与适用边界
解出 9 个问题的另一面，是剩下 344 个没有解出来：9/353，成功率约 2.5%。据 the-decoder 德语版报道，成功集中在 Lean 数学库 Mathlib 较为成熟、问题可以拆成可处理子目标的领域——组合数学、凸优化和数论；大多数埃尔德什问题仍然够不着，「更不用说需要大量新理论的问题」，而且 agent 会继承底层语言模型的不可靠性。报道还提到，陶哲轩（Terence Tao）曾提醒，AI 在埃尔德什问题上的真实成功率只有 1%～2%，且集中在较容易的题目上；Google 系统的 9/353，基本对应他说的这道约 2% 的门槛。
在六个已解出的埃尔德什问题上，论文比较了四种 agent 的解题率与平均成本：在 erdos_26 这类较容易的题目上，四个版本都能达到高成功率；在 erdos_125、erdos_152 这类难题上，满配的 D 有时用更少尝试解出，而预算充足的 A 最终也能到达。
与系统合作的数学家报告说，连失败的证明尝试也加深了他们对问题的理解：因为草稿是形式化的，专家可以直接跳到未解决的子目标，而不必重查整个论证。这些 agent 还被用来揪出文献中已有的形式化错误，研究者写道，形式验证「可以充当过滤器，判断哪些证明值得人工复核」。
期刊评审与 GitHub 批量放出：两条发布路线
这项研究发表在一轮激烈争论之中。10 月 7 日，OpenAI 把内部前沿模型生成的 ，而不是投给学术期刊；据 the-decoder 报道，每份结果平均耗用约 3 小时的 ChatGPT Pro 算力，许多附有 Lean 形式化以便机器核验，OpenAI 称其中包含与黎曼猜想相关的进展。
第二天，由菲尔兹奖得主陶哲轩担任主席的 AHM 呼吁数学家抵制 OpenAI，声明把一次性放出如此多的文件称作「不是学术的展示，而是力量的展示」；同一份 the-decoder 提到，OpenAI 在发布次日因一处符号错误撤回了三篇论文。DeepMind 走的是另一条路：先在网上公开解法，再让论文接受同行评审；OpenAI 的那批结果则仍留在 GitHub 上，等数学界逐份核对。至于 AlphaProof Nexus 这次尝试的其余 344 个埃尔德什问题，依然无解。