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氪经授权发布。