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

这个月的数学界，可以说是彻底沸腾了。

前脚OpenAI刚用自然语言推理推翻了埃尔德什的一个80年猜想，数学家们的惊叹声还没散去。紧接着，Google DeepMind就亮出了另一张王牌——全新的AI数学智能体

。

它的首秀堪称震撼：一口气解决了

悬而未决数十年的。其中最难啃的一块骨头，已经。

更关键的是，这次的结果拥有无可辩驳的确定性。因为每一个证明步骤都经过了Lean编译器的形式化验证，不存在任何“幻觉”或逻辑漏洞的空间——编译器通过，证明即为正确。而且，解决每道题的平均算力成本，

。

值得注意的是，这次的AlphaProof Nexus与2024年那个在国际数学奥林匹克竞赛中摘银的初代AlphaProof截然不同。初代主要依赖强化学习树搜索，而Nexus则融合了大语言模型、AlphaProof和进化算法，其目标直接对准了人类数学家都感到棘手的研究级难题。

AlphaProof Nexus：三合一架构如何运作

这套系统的设计思路清晰，采用了一种分层递进的架构，从简单到复杂，共分为四个层级。

：这是最朴素的版本。多个独立的证明子智能体并行工作，每个智能体与Gemini 3.1 Pro模型进行多轮对话。它们通过搜索和替换工具来修改Lean代码，Lean编译器则实时提供错误反馈，智能体据此迭代修正。

：在A的基础上，引入了AlphaProof作为“外援”工具。当子智能体在某个子目标上卡壳时，可以调用AlphaProof进行强化学习驱动的树搜索，尝试攻克局部难点。

：引入了进化算法的思想。多个子智能体不再单打独斗，而是共享一个“种群数据库”。每个生成的证明草稿会由一个大语言模型评审员进行打分（采用类似国际象棋的Elo评分系统），高分的草稿会被优先采样，进行变异和“进化”。

：这是集大成的最终形态，融合了进化算法、AlphaProof和Gemini 3.1 Pro，协同作战。DeepMind正是用这个版本大规模扫荡了埃尔德什问题。

整个工作流程形成了一个高效的核心循环：AI提出证明草稿 → Lean编译器验证 → 若失败则反馈错误信息 → AI根据反馈修正 → 再次提交验证。这个过程循环往复，直到证明完全通过，或者达到预设的算力预算上限。

以

的解决过程为例，可以清晰地看到这种协作：子智能体首先用思维链推理分析问题结构，然后通过搜索替换修改Lean代码，接着调用AlphaProof处理其中的子目标。

AlphaProof成功解决了6个子目标中的3个。随后，子智能体将剩余的几个“硬骨头”进一步分解为更小的引理，再次调用AlphaProof——这一次，所有难题被一举攻克。整个过程，没有任何人类数学家的直接介入。

九道难题告破，最老悬案终结

DeepMind将完整版的Agent D投向了353个已经形式化的埃尔德什问题，每道题最多允许进行3000轮迭代尝试。

最终，有9道长期悬而未决的问题被成功攻克。

其中几道问题的含金量尤其高：

这个问题悬置了56年，期间多位数学家取得了部分进展，但始终无法给出完整的构造。AI的解法精妙地结合了中国剩余定理和三项等差数列回避集，通过构建一系列精心设计的“区块”，同时满足了密度条件和整除约束。

AI证明了其下密度为零。证明的核心是一个归纳稀疏化论证，巧妙地利用了3^m和4^k的丢番图逼近性质（因为log4/log3是无理数），通过反复找到两个基数几乎对齐的尺度，让密度以0.99的比率逐步衰减到零。

AI给出了一个极其优雅的证明：W(k+1) ≥ W(k) + k。核心思路是贪心染色扩展——在一个没有单色k项等差数列的2-着色基础上，逐个添加新元素，并用反证法说明贪心策略不会失败。

这是一个关于平面点集中共线性质的问题。AI的构造令人叹为观止：它将完全图K∞的每条边映射到平面上的一个点，用二次多项式编码坐标，然后利用无穷拉姆齐定理完成了证明。

目前，这9道问题的完整Lean证明代码均已开源。

简单智能体也能解全部难题？

整个研究中最出人意料的结论，或许不是完整版Agent D的强大，而是：

Agent A既没有进化算法，也没有AlphaProof作为工具，它仅仅依靠多个独立的大语言模型子智能体与Lean编译器的反馈循环。根据DeepMind团队的对比分析，在大多数问题上，Agent A与加入了AlphaProof的Agent B表现几乎在误差范围内相同。

相比之下，Agent D的优势主要体现在最困难的问题上（例如#125和#138），它能以2到5倍的成本优势完成证明。

对此，DeepMind将基础智能体的成功归因于两个关键因素：大语言模型自身能力的飞速提升，以及编译器反馈在锚定和纠正模型推理方面的强大作用。

这暗示了一个有趣的趋势：随着基础模型越来越强，今天需要复杂系统工程（进化算法、专用工具）才能高效解决的问题，未来可能一个朴素的“大语言模型+编译器”反馈循环就足够了。当然，前提是用对了模型——实验表明，单独运行AlphaProof或使用较小模型（如Gemini 3.0 Flash），这9道题一道也解不出来。

具体到成本，最便宜的一道题（#741(ii)）中位成本仅5-7美元，最贵的（#152）也不过200-400美元。

跨界突破：从代数几何到凸优化

AlphaProof Nexus的“战绩”并不局限于埃尔德什问题。它在多个数学分支中都取得了实质性突破：

系统自动形式化了492个开放猜想，并证明了其中44个。为防止形式化错误，系统设置了一个巧妙的前置条件：必须先证明一个“测试引理”——验证序列的前几项与形式化定义一致——才能尝试证明目标猜想。

解决了一个悬置约15年的开放问题，证明了余维数3、类型2的纯O-序列的对数凹性。这个问题此前被认为是该领域最后一个主要的未解情况。

解决了一个关于锚定梯度下降-上升算法精确收敛速率的开放问题。更妙的是，AI不仅在验证一个固定算法，还在证明过程中自主搜索并发现了一个新的学习率调度参数，从而实现了更强的性能保证。

证明了Graffiti系统在1996年提出的一个关于生成树叶子数与局部独立集的猜想，形成了一个有趣的闭环——一个AI证明了另一个AI在近三十年前提出的猜想。

帮助解决了本·格林著名开放问题列表中的第57题。

与Mario Krenn合作，解决了多个关于单色量子图的猜想，这些猜想对应着高维GHZ量子态的构造。

三路合围：数学研究范式正在重塑

2026年5月，AI在数学研究领域的能力，几乎同时从多个方向达到了前沿水平。

其通用推理模型直接输出人类可读的证明，推翻了埃尔德什的单位距离猜想。证明本身极其精妙，但验证它需要人类顶级专家逐行审查。菲尔兹奖得主高尔斯曾将未解问题抛给GPT-5.5 Pro，两小时内就获得了博士论文级别的成果，而他在过程中的数学贡献几乎为零。

AlphaProof Nexus让AI用Lean语言编写证明代码，由编译器自动检查每一步推理。任何一步出现逻辑断裂，编译器直接报错，证明即被拒绝。这条路线可靠性极高，但现阶段受限于Lean数学库已经成熟的领域。

自然语言路线灵活，但可能存在幻觉；形式化路线可靠，但门槛较高。而DeepMind的数学家合作者还发现了一个意料之外的收获：即使智能体最终未能证明目标定理，它生成的形式化证明尝试也极大地加深了人类专家对问题的理解。因为草稿是形式化的，专家可以直接聚焦于未解决的子目标，而不需要从头重新验证整个论证链。

换句话说，AI不只是在解题，它正在潜移默化地改变数学家思考和研究问题的方式。

如今，未来的图景已经逐渐清晰：AI先用自然语言灵活地探索证明思路和灵感，再用形式化系统逐步将思路固化为严谨、可验证的代码。而人类数学家的角色，则可能从“亲手推导每一步”转向“提出关键问题、审查研究方向、提炼深层洞见”。

AI先用自然语言探索证明思路，再用形式化系统逐步固化和验证。
人类数学家的角色，则从「亲手推导」转向「提出问题、审查方向、提炼洞见」。

有人说，我们正在目睹数学“奇点”的早期火花。几百美元的算力，几十小时的运行，56年的悬案就此告破，编译器给出了铁一般的证据。

保罗·埃尔德什生前留下了1217道数学难题，悬赏后人求解。他大概从未想过，有一天来“领赏”的，并非人类。