人类56年解不出，谷歌AI一夜连破9道世纪难题！

新智元报道 【新智元导读】 DeepMind发布全新数学智能体AlphaProof Nexus，9道Erdős开放难题一次性告破，最老的悬了56年！全部证明都已经过Lean编译器形式化验证，没有幻觉。网友惊呼：数学奇点的火花点燃了。 数学界这个月，彻底疯了。 前脚OpenAI刚把Erdős 80年猜想推翻，数学家们的惊呼声还没落地。 紧接着，Google DeepMind发布了一个全新AI数学智能体—— AlphaProof Nexus 。 论文地址：https://arxiv.org/abs/2605.22763v1 它一出手，就干掉了 9道 悬而未决几十年的 Erdős开放问题 。其中最古老的那个， 悬了整整56年 ！ 而且，每道题花费的算力成本， 只有几百美元。 更关键的是， 这次的证明不可能有错 。 每一步推理都经过Lean编译器的形式化验证，不存在幻觉空间。编译器通过，证明就是对的。 值得一提的是，AlphaProof Nexus和2024年拿下IMO银牌的初代AlphaProof完全不同。 初代只有强化学习树搜索，Nexus把大语言模型、AlphaProof和进化算法三合一，直接瞄准了人类数学家啃不动的研究级难题。 AlphaProof Nexus 进化算法+LLM+Lean编译器 这套系统的架构分为四个层级，从简单到复杂。 1. Agent A（基础版） 多个独立的证明子智能体并行工作，每个子智能体与Gemini 3.1 Pro进行多轮对话，通过搜索替换工具修改Lean代码，编译器实时反馈错误信息，子智能体根据反馈迭代修正。 2. Agent B 在A的基础上加入了AlphaProof作为工具。当子智能体在某个子目标上卡住时，可以调用AlphaProof进行强化学习驱动的树搜索，尝试攻克局部难点。 3. Agent C 引入进化算法。多个子智能体不再独立工作，而是共享一个「种群数据库」。每个证明草稿会被LLM评审员打分（用Elo评分系统），高分草稿被优先采样、变异、进化。 4. Agent D（完整版） 集大成者。进化算法 + AlphaProof + Gemini 3.1 Pro协同作战。这是DeepMind用来大规模扫荡Erdős问题的主力武器。 整个工作流的核心循环非常清晰—— AI提出证明草稿 → Lean编译器验证 → 失败则反馈错误信息 → AI修正 → 再验证 → 循环往复，直到证明完全通过或耗尽算力预算。 以 Erdős #125 为例，它的解题过程是这样的。 首先，子智能体先用思维链推理分析问题结构，然后通过搜索替换修改Lean代码，接着调用AlphaProof处理子目标。 AlphaProof搞定了6个子目标中的3个，子智能体随即将剩余的「硬骨头」分解为更小的引理，再次调用AlphaProof——这次，全部搞定。 整个过程中，没有任何人类数学家介入。 9道Erdős问题 56年前的悬案一朝告破 DeepMind将完整版Agent D投放到353道已形式化的Erdős问题上。每道题最多允许3000轮迭代。 最终，9道问题被攻克。 其中含金量最高的几道： 1. Erdős #12（1970年提出） 是否存在一个无限集A，满足「任意三个不同元素a 这道题悬置了56年，期间多位数学家取得了部分进展，但始终无法给出完整构造。 AI的解法精妙地结合了中国剩余定理和三项等差数列回避集，通过构建一系列精心设计的「区块」来同时满足密度条件和整除约束。 2. Erdős #125（1996年提出） 在三进制下只用数字0和1的整数集A，加上四进制下只用数字0和1的整数集B，它们的和集A+B的下密度是否为正？ AI证明了答案是否定的——下密度为零。 证明的核心是一个归纳稀疏化论证，巧妙利用了3^m和4^k的丢番图逼近性质（log4/log3是无理数），通过反复找到两个基数几乎对齐的尺度，让密度以0.99的比率逐步衰减到零。 3. Erdős #138（1981年提出的变体） van der Waerden数W(k+1) - W(k)是否趋于无穷？ AI给出了一个极其优雅的证明：W(k+1) ≥ W(k) + k。核心思路是贪心染色扩展——在一个没有单色k-AP的2-着色基础上，逐个添加新元素，用反证法说明贪心策略不会失败。 4. Erdős #846 这是一个关于平面点集中共线性质的问题。 而AI的构造，令人叹为观止。 它把完全图K∞的每条边映射到平面上的一个点，用二次多项式编码坐标，然后利用无穷Ramsey定理完成证明。 目前，所有9道问题的Lean证明代码已开源在GitHub上。 项目地址：https://github.com/google-deepmind/alphaproof-nexus-results 简单Agent也能解全部9题？！ 最出人意料的结论，不是完整版Agent D有多强，而是—— 最简单的Agent A，也能解决全部9道问题。 Agent A没有进化算法，没有AlphaProof，只有多个独立的LLM子智能体和Lean编译器的反馈循环。 根据DeepMind团队的对比分析，它在大多数问题上，Agent A和Agent B（加了AlphaProof的版本）的表现在误差范围内几乎相同。 相比之下，Agent D的优势主要体现在最困难的问题上（比如#125和#138），能以2到5倍的成本优势完成证明。 对此，DeepMind将基础Agent的成功归因于两个因素：LLM自身能力的飙升，以及编译器反馈在锚定LLM推理方面的强大作用。 也就是说，随着基础模型越来越强，复杂的系统工程可能逐渐让位于简单的智能体循环。 今天需要进化算法和AlphaProof协同作战才能高效解决的问题，明天可能一个朴素的LLM+编译器循环就够了。 具体到成本，最便宜的一道题（#741(ii)）中位成本仅5-7美元，最贵的（#152）也不过200-400美元。 但前提是用对了模型——单独运行AlphaProof或使用较小模型（Gemini 3.0 Flash等），9道题一道都解不出来。 代数几何15年悬案、凸优化新界一并搞定 除了Erdős问题，AlphaProof Nexus还在多个数学分支中取得了实质性突破： OEIS猜想 ： 系统自动形式化了492个开放猜想，证明了其中44个。为防止形式化错误，系统要求先证明「测试引理」——验证序列前几项与形式化定义一致——才能尝试目标猜想。 代数几何 ： 解决了一个悬置约15年的开放问题——证明了余维数3、类型2的纯O-序列的对数凹性。这个问题此前被认为是该领域最后一个主要未解情况。 凸优化 ： 解决了一个关于锚定梯度下降-上升算法（Anchored GDA）精确收敛速率的开放问题。更妙的是，AI不仅验证了一个固定算法，还在证明过程中自主搜索并发现了一个新的学习率调度参数，从而实现了更强的保证。 图论 ： 证明了Graffiti系统在1996年提出的一个关于生成树叶子数与局部独立集的猜想，形成了一个有趣的闭环——AI证明了另一个AI提出的猜想。 加法组合学 ： 帮助解决了Ben Green著名开放问题列表中的第57题。 量子光学 ： 与Mario K