数学界刚刚迎来了一次标志性的同行评审。2026 年 10 月 8 日，Google DeepMind 团队第一作者 George Tsoukalas 等人的研究正式刊载于《Science》正刊（预印本于 2026 年 5 月 21 日披露），宣布其 AI 架构 AlphaProof Nexus 攻克了 353 个已形式化的 Erdős 猜想中的 9 个，其中两道悬置长达 56 年。此外，该系统还证明了 OEIS 整数序列数据库中的 44 个猜想，解决了一道代数几何开放问题，并优化了 min-max 优化的已知上界。
这一突破最引人注目的地方不在于解题数量，而在于路径选择：在数学推导极易产生自然语言幻觉的当下，DeepMind 放弃了纯文本大模型的自由发挥，将推理全面框定在形式化验证系统 Lean 之中。与此同时，OpenAI 将包含 372 个成果族的自然语言手稿批量倾倒在 GitHub 上，引发人类数学协会（AHM）公开发表客座声明抗议。两家机构的巨大分歧，让纯数学成了大模型可靠性推理竞争中最激烈的一块试验田。
9 道难题背后的真实命中率与算力修辞
公众看到的标题往往是机器攻克半个世纪未解难题，但技术细节里的数字描绘了另一幅图景。AlphaProof Nexus 面对 Erdős 猜想的真实解决率仅为 2.55%（353 题中解决 9 题），面对 OEIS 猜想的解决率也只有 8.94%（492 题中证明 44 题）。
更重要的是，这 9 道题并非全都是 Erdős 当年抛出的原始完整命题。它们大部分是命题的子问题或变体，包括 #12(i)、#12(ii)、#125、#138 变体、#152、#741(i)、#741(ii)、#846，以及非 Erdős 本人提出的 #26 变体。数学社区维基显示，部分结果如 #152 此前已有类似文献，#846 与 OpenAI 的探索独立重合，而 #26 仅仅是加强了已有结论。这并不意味着成就被打折扣，而是表明机器解决的是精细切割后的数学切片，而非全局性的理论构建。
外界流传的“单题成本仅几百美元”同样存在显著的统计修饰。在 DeepMind 的基准测试中，核心驱动引擎 Gemini 3.1 Pro 搭配 Lean 的报错反馈机制，实际上已经能够解出这 9 道题。Nexus 架构的加入，主要是在疑难案例上优化搜索效率。但官方图表公布的低廉成本，既排除了疑难子任务调用专用证明工具 AlphaProof 时单题约 27.5 TPU-hours（约 60 美元）的推理开销，更完全略过了在其余 344 个未解目标上进行全量试错、反复穷举所消耗的算力总账。
- 提醒.宣称低成本解题的前提是只计算命中目标的单次推演，如果将 97.45% 失败尝试的试错算力纳入分摊，AI 发现数学定理的边际成本依然昂贵。
自主神话之下：人机协作的翻译屏障
公众容易将该成果想象成一个端到端的自主超人数学家，但这忽略了整个证明链条中最繁重的人工介入环节。AlphaProof Nexus 的运行依赖于奥胡斯大学 Gergely Bérczi 等人类数学家的深度配合。
在大模型接手之前，人类数学家必须先完成形式化翻译：将数学自然语言转化为严格的 Lean 语法，并修正定义偏差。例如在 Erdős 猜想的 #125 与 #741(i) 中，人类学者专门更正了命题中关于密度的数学定义偏差。模型虽然可以在代码空间内完成无监督搜索，但一旦它排除了所有占位符（消除 sorry 标记）完成编译，这些冗长、机器特化的代码依然无法直接被学术界阅读，仍需要人类数学家重新反向撰写自然语言可读论文。
机器负责的是规则完备后的巨大搜索空间，而决定问题怎么提、如何才算没有偏离数学本意的钥匙，依然握在人类研究者手中。
路线之争：严格编译对撞粗暴倾倒
这篇发表在《Science》上的论文，正好撞上了学术界关于机器证明治理规则的敏感时刻。
不久前，OpenAI 向 GitHub 倾倒了多达 719 篇未经传统同行评审的手稿，将其归纳为 372 个成果族，宣称要让学术界跟上步伐。然而这批成果中，仅有约 42% 的顶级成果经过了 Lean 的形式化验证，剩余 58% 依然是未经代码级校验的自然语言推导，OpenAI 甚至在附注中坦承推导可能存疑。
这种将海量未经形式化验证的半成品推给学界的做法激怒了研究人员。人类数学协会（AHM）公开发表声明，呼吁数学家停止与 OpenAI 合作。尽管部分流传将陶哲轩描绘为抵制发起人，但事实是陶哲轩仅在其个人博客代发了该客座声明，并非抗议的主导者。
数学界抗议的不是人工智能本身，而是利用未经代码级检验的伪推导稀释学术公地的行为。
机器证明时代最根本的学术分歧，在于谁来为推导错误的核验成本买单。
DeepMind 顺应了数学界的根本诉求：大模型生成的草稿只要没有通过 Lean 编译系统的真值检验，就绝不当作真理输出；一旦完全消除编译占位符，其逻辑正确性就得到了数学机器的刚性背书。
- 结论.将机器证明与代码编译器深度绑定，并提交权威同行评审，正在成为 AI 进入严谨科学领域的准入门槛；单纯堆砌自然语言思维链的做法正在失去严肃学界的信任。
纯数学是目前少数能够为 AI 推理提供零歧义即时真值反馈的封闭沙盒。随着 Lean 成为人机交互的事实标准，机器确实展现出了协助拓展人类认知边界的潜力。但在解决率突破个位数之前，学术界真正需要提防的，并非 AI 过早取代数学家，而是未经形式化淬火的海量生成物提前淹没人类有限的审稿精力。