DeepMind AlphaProof Nexus登《Science》：AI自主破解多道56年未解Erdős数学难题
最近，AI 数学圈的戏很足。10 月 6 日，OpenAI 往 GitHub 上一次性倾倒了 722 篇 AI 生成的数学手稿，数学界当场炸锅，陶哲轩牵头的人类数学协会（AHM）发声明呼吁抵制。
就在同一个星期，Google DeepMind 的一篇论文登上了 10 月 8 日的《Science》，走完了正经的同行评审。
据媒体报道，这篇论文的主角叫 AlphaProof Nexus，一个自动寻找数学证明的系统。成绩是：353 道悬而未决的 Erdős 问题，它自主解出了 9 道，其中两道从 1970 年摆到现在，有 56 年。
论文地址：https://www.science.org/doi/10.1126/science.aej2213
Erdős 问题是以匈牙利数学家保罗·埃尔德什命名的一批开放问题，主要散布在组合数学和数论里，他生前还喜欢给难题明码标价挂悬赏。这批问题如今是检验 AI 数学能力的试金石。
有个细节，这 353 道题里可没有 DeepMind 自己挑的软柿子，它们就是开源社区在 Formal Conjectures 仓库里已经翻译成 Lean 语言的全部 Erdős 问题（截至 2026 年 2 月），系统照单全收，每道题最多尝试 3000 轮，证不出来就放弃。最后中的 9 道里，包括 Erdős 和 Sárközy 1970 年提出的第 12 题。
成绩单还不止这一栏：OEIS 整数序列百科全书里的开放猜想，492 道证出 44 道；一个悬了 15 年的代数几何问题（关于希尔伯特函数的猜想）被解决；在 min-max 优化里找到了一个没人想到过的参数调节方案，改进了已知上界。另外，它还帮着攻克了数学家 Ben Green 清单上的一道开放问题，目前正被拿去支援量子光学和图论的在研项目。
成本方面，论文给出的数字是每道题几百美元的推理开销。
它是怎么证的
核心循环一句话就能说清：大模型负责写，编译器负责判。
具体来说，Gemini 3.1 Pro 用 Lean 这种形式化语言起草证明，每改一版，Lean 编译器就逐行检查一遍，报错信息反回去，指导下一稿。系统还有几道保险：定理陈述一个字不许改，证明里不许留"sorry"占位符，不许私加公理，整个验证在沙盒里运行。
在这个循环之上，研究团队还搭了个"进化"班子：一群子代理各自搜证，用类似下棋的 Elo 评分互相锦标赛，有前途的思路留下，死路删掉；遇到硬骨头子问题，可以呼叫 AlphaProof，就是 2024 年拿下国际奥数银牌水平的那个专用证明器。
AlphaProof Nexus 的工作流程：数学家提供自然语言背景、Lean 形式化题目和知识库，系统内部的证明子代理、评审子代理和验证器围绕一个"种群数据库"循环迭代，最终产出形式化证明。
不过论文里有个挺实在的消融结果：把花哨的架子拆掉，只留"大模型加 Lean 反馈"的简版系统，9 道 Erdős 题也都能解出来，只是最难的几道更烧钱。换句话说，主要功臣是基础模型和编译器反馈这个组合本身。
六道 Erdős 问题上的解题率与平均成本。蓝线是简版系统，橙线是加了 AlphaProof 的版本，红三角是完整系统。大多数题目的求解成本在几十到几百美元之间。
泼几瓢冷水
第一，命中率。353 中 9，大约 2.5%。这个比例和陶哲轩估计的"AI 解 Erdős 问题的成功率大概在百分之一二"基本吻合。绝大多数开放问题它仍然够不着，论文自己也承认，成功集中在 Lean 数学库比较成熟的领域，需要大量新理论的问题还谈不上。
第二，计数可能有水分。论文公开了全部 Lean 证明之后，有独立审计发现，第 846 题虽然证明本身成立，但早些年 Reiher、Rödl 和 Sales 的一个定理其实已经蕴含了答案。按更严格的"新解决"定义，9 应该改成 8。另外第 741 和 846 题，OpenAI 的内部模型也独立解出来过。
第三，系统不开放。证明文件挂在 GitHub 上任人下载，但 AlphaProof Nexus 本身不对外用，别人没法亲手复现。DeepMind 的 CEO Hassabis 也早早表态，说这仍然不是 AGI。
值得玩味的是发表的时机和方式。
OpenAI 那边，10 月 6 日把 722 篇手稿堆上 GitHub，覆盖 372 个结果系列，号称参考了普林斯顿高等研究院独立咨询小组的建议。结果一天之内就有 3 篇因为符号错误撤回。
陶哲轩担任主席的 AHM 随后发声明，批评这是一场力量展示，呼吁数学家抵制。10 月 9 日，陶哲轩在自己博客上转发了数学家 Thomas Hales 的专栏文章《数学家应该了解的 Lean 定理证明器：可靠性与人工智能问题》。
DeepMind 这边，5 月 21 日先挂在预印本上，然后把解答提前公开在 ErdosProblems 论坛上让行家围观挑错，最后把论文送进了《Science》的同行评审流程。那 9 道题的 Lean 证明，也早就登记在陶哲轩维护的"AI 对 Erdős 问题贡献" wiki 页面上。
本文来自微信公众号“大数据文摘”，36氪经授权发布。