Google DeepMind 的数学证明系统 AlphaProof Nexus 正式发表在 Science 上。论文第一作者署名 Tsoukalas，研究团队全部来自 DeepMind。这项工作 5 月底先以预印本公开过，这次是经过同行评审后的期刊版本。
成绩单不变：系统尝试了 353 道尚未解决的 Erdős 问题，解出 9 道，其中 2 道已经悬了 56 年；在整数数列数据库 OEIS 的 492 个开放猜想里证出 44 个；另外还回答了代数几何里一个关于 Hilbert 函数、悬置约 15 年的问题，并改进了 min-max 优化里的一个已知界。
一个 Gemini，一个 Lean 编译器
系统的底座是 Gemini 3.1 Pro。模型用形式化语言 Lean 起草证明，Lean 编译器每改一步就检查一次，报错信息直接喂回给下一轮尝试。整个过程中，人只在最后看结果。
论文里拆出了四个版本：
- A 版：最朴素的“生成—验证”循环，大模型写，编译器判；
- B 版：在 A 的基础上接入 DeepMind 此前的证明器 AlphaProof，专门补证明里缺的片段；
- C 版：加入进化机制，多个子智能体共享一池证明草稿，用 Elo 分排序；
- D 版：以上全部叠加，用来打 Erdős 问题。
结果里最耐人寻味的一条，是 A 版也独立证出了全部 9 道 Erdős 题，只是在最难的几道上花的钱更多。The Decoder 援引的推理成本是每道题几百美元。作者在论文里的说法是：
“power of compiler feedback in grounding LLM reasoning” （编译器反馈能把大模型的推理钉在实处。）
西班牙学者的几处保留
西班牙科学媒体中心在论文上线当天找了几位当地学者点评，意见分成两边。
UAM 研究员 Pablo Haya Coll 认为，这套方法能系统性地产出有分量的数学发现。UOC 的 Josep Curto 给出的评价是 “a dazzling display of technical capability marred by significant methodological inconsistencies”，大意是技术上令人眼花缭乱，方法上却有明显的前后不一。他列了三点：A 版和 D 版解出同一批题，说明框架复杂度未必决定发现能力；成本只算了成功的那些运行，B 版和 D 版的账里也没有计入 AlphaProof 自身的推理开销；Lean 只能保证证明对“写下来的那条命题”成立，命题本身有没有忠实翻译原题，仍然要靠数学家人工核对，论文也承认出现过形式化错误。
ICMAT 所长 Javier Aramayona 担心的是另一件事：一大批“已知为真、却没人完全读懂”的结果开始出现，数学研究里理解的那一环、年轻研究者的训练过程，都可能被削弱。巴利亚多利德大学的 Teodoro Calonge 则说得更直接，这个领域还有相当大的改进空间。
作者自己也写明了范围：AI 在 Erdős 问题上的整体成功率大约在 1% 到 2%，解出的多是相对容易的题，集中在组合、凸优化和数论这些 Mathlib 库积累较厚、问题好拆成子目标的方向。需要发明大量新理论的问题，系统基本碰不到。
把今年几件事串起来看
5 月，本站报道过 OpenAI 模型攻克一个 80 年的 Erdős 猜想；9 月，数学家与 OpenAI 之间又起过一场署名之争；10 月 6 日，OpenAI 在 GitHub 上一次性放出 722 篇 AI 生成的数学手稿，用的是开源仓库加 Apache 2.0 许可，没有走期刊。The Decoder 的报道提到，由陶哲轩牵头的一个数学家团体随后呼吁抵制这种做法。
两家公司的路径差别在这里摆得很清楚。OpenAI 选择量大、公开、让社区自己去筛；DeepMind 选择数量少得多，但每一条都过了 Lean 编译器，又过了期刊审稿。后者在论文里给 Lean 的定位也很克制，原话是形式化验证 “can serve as a filter for determining which proofs merit human review”，即用来决定哪些证明配得上人去看。
粗算一下：按每题几百美元算，9 道 Erdős 题的推理开销远低于一个博士后一个月的薪水；可按 Curto 指出的口径，失败的运行和 AlphaProof 的调用加进来之后，账面会大多少，论文目前没有给出数字。DeepMind 已经把证明和部分说明放在 GitHub 的 alphaproof-nexus-results 仓库里，外部数学家可以逐条去对。
参考来源：Science 期刊论文、The Decoder、CocoLoop、西班牙科学媒体中心专家点评；论文正文核验 353 道 Erdős 问题解出 9 道、492 个 OEIS 猜想证出 44 个及四个智能体版本的分工。