AI进军数学界的速度，远超许多人的预料。
OpenAI前脚刚用内部模型突破了埃尔德什80年未解的单位距离问题，谷歌DeepMind后脚就端出了一套全新的证明框架——AlphaProof Nexus。这套由 Gemini 驱动的智能体系统，一口气解决了涵盖数论、组合几何等领域的9个埃尔德什开放问题。其中最古老的一个猜想，已困扰数学界整整56年。
除了埃尔德什猜想，AlphaProof Nexus 还顺手证明了OEIS整数序列百科里的44个猜想，攻克了一道搁置15年的代数几何难题，并改进了凸优化领域中一个沿用已久的理论边界。
更引人注目的是它的推理成本：平均每解决一道题，算力开销仅为几百美元，且整套证明代码已在 GitHub 全面开源。
值得一提的是，这篇论文作者阵容达到20人，其中就包括2016年 AlphaGo 的核心研究员 Aja Huang。从围棋到纯数学，DeepMind 似乎正在将强化学习与形式化验证推向更多未知领域。
56年无人破解的难题，AI给出了什么答案？
AlphaProof Nexus 解决的这9个问题各具挑战。我们挑其中三道，一起感受下这些猜想的难度与AI解法的精妙之处。
Erdős #12，1970年提出，悬置56年
这道题的核心要求是构造一个具备特殊性质的无限整数集合。该集合必须满足两个近乎矛盾的条件：
- 集合中任取三个不同的数 a、b、c，a 绝不可能整除 b + c 的和。
- 这个集合不能过于稀疏，在自然数中必须维持一定的密度。
简单说，数字之间既不能出现“整除”关系，也不能出现“一个数整除另两个数和”的情况，同时数字还要分布得相对密集。从1970年起，数学界始终无法给出这个集合的完整构造。很多研究取得了局部进展，但始终缺少一个能把所有条件串联起来的全局解。
AI的解决思路颇具层次感。它调用中国剩余定理，将看似无法驾驭的全局问题拆解为众多独立的“区块”。每个区块内部，系统用三项等差数列的回避集来满足局部整除约束，最终把所有区块拼合成满足全部条件的无限集合。这种方法将一个看似只能硬凑的组合问题，降维成了可控的模块化构造。
Erdős #125，1996年提出，沉寂近30年
这道题的表述极其简洁，但难度极高。想象两个数字集合：
- 集合 A：所有在三进制下仅由数字 0 和 1 组成的非负整数。
- 集合 B：所有在四进制下仅由数字 0 和 1 组成的非负整数。
将 A 和 B 中的数字两两相加，得到一个新集合 A + B。问题来了：A + B 中的数字在自然数中出现的频率（数学上称为下密度）是否为正？
直觉上，A 和 B 本身已经是相当稀疏的集合，它们的和集应该更稀疏才对。但这个稀疏有没有到密度彻底归零的程度？自1996年提出以来，这个问题始终没有定论。
AI给出的答案是：密度为零。
证明的核心依赖于一个深刻的数论事实：log₄ / log₃ 是一个无理数。这意味着 3 的幂次和 4 的幂次能够以任意精度彼此逼近。利用这一点，AI构造了一个巧妙的归纳性稀疏化论证：通过不断寻找两个几乎对齐的尺度（即 $3^m \\approx 4^k$），让密度以 0.99 的比率一步步衰减，最终趋近于零。一个纯粹的数论性质，竟成了破解组合谜题的钥匙，确实令人叹服。
Erdős #846，1992年提出，卡了人类34年
这是一道痛击人类直觉的组合几何问题。AI需要证明，存在这样一个无限扩展的平面点集：
任意选出有限个点来看，你总能发现其中大部分点是不共线的——每个局部切片都显得很正常。但如果你试图把这个无限集合拆分成有限个“绝对没有任何三点共线”的子集时，根本办不到。
一个集合的每个有限片段都规规矩矩，但作为一个整体，它却顽固得拒绝任何“不共线”的拆分。这种局部与全局之间的张力，正是组合几何中最令人头疼的那一类挑战。
AI的策略是将几何问题翻译成图论与逻辑的语言。它把完全图的每条边映射到平面上一个点，利用二次多项式编码坐标，最后借助无穷拉姆齐定理完成证明。这种跨领域的知识迁移能力，是否让你也开始思考，形式化证明的未来究竟会通向何方？
除了这三道，AlphaProof Nexus 在整除集构造、范德瓦尔登数间隙、西顿集孤立点、集合拆分密度等领域也分别解决了另外六项埃尔德什猜想。
与此同时，AlphaProof Nexus 还在OEIS整数序列百科中证明了44个开放猜想，在代数几何领域解决了希尔伯特函数对数凹性这个搁置了15年的问题，并在凸优化中改进了锚定梯度下降法的理论边界。
菲尔兹奖得主陶哲轩曾客观评估，AI目前攻克埃尔德什问题的实际成功率大约在1-2%。这一次，谷歌的系统挑战了353道题，解开了9道，比例恰好落在了这个区间内。这说明，距离全面攻克这类问题，路还很长，但通往未知的门，已经被推开了一道缝。
几百美元算力，撬动一道56年未解之题
AlphaProof Nexus 的架构核心，可以用一句话概括：Gemini 3.1 Pro 生成 Lean 语言证明步骤 → Lean 编译器逐行检查 → 报错直接反馈给模型 → 模型根据报错修改 → 再检查 → 循环直到全部通过。
这种感觉，是不是很像平时写代码，只不过现在 Debug 的对象，换成了数学定理？
在这套框架里，DeepMind 设计了四种复杂度递进的 Agent 工作模式。
最简单的 Agent A，同时启动多个独立子智能体。它们先靠 Gemini 3.1 Pro 梳理解题思路，动手编写证明代码，写完立刻交由编译器核验。一旦报错，错误信息会原封不动地传回模型，驱动它不断修改、重试，直到通关。全程没有调用任何额外辅助工具，纯靠“写代码—查错—改正”这个闭环。
Agent B 加入了一个强力外援：AlphaProof。 AlphaProof 是 DeepMind 此前专为奥数级别题目训练过的强化学习证明工具。当 Agent A 的模式在某个小目标上反复卡壳，编译器持续报错也无法自我修复时，Agent B 便能调用 AlphaProof 进行一次强化学习驱动的树搜索，专门攻击这个顽固的局部难点。
Agent C 引入了进化算法的思路。 前面两种模式中，各个子 Agent 都是独立工作、互不交流。Agent C 则让所有子 Agent 共享一个“证明草图种群”。每一个子模块都会产出不同的证明草稿，然后系统会从“合理性、清晰度、新颖性”三个维度给每份草稿打分，采用 Elo 评分系统进行排名。高分草稿会相互“交配”、组合，衍生出新解法，低分草稿则直接淘汰。整个种群在浩瀚的证明空间里进行了一场定向进化。
Agent D 是完全体： 进化筛选思路 + 专项工具（AlphaProof）攻克难点 + 大模型逻辑推理，三股力量在统一架构内协同作战。它也正是这次批量破解难题的主力。
看到这里，我本以为最强的 Agent D 会全面碾压，而 Agent A 只是作为实验对照组的“炮灰”。
但论文给出的结果却出乎意料：结构最简单的 Agent A，同样能够独立解出全部9道题。
没有进化算法，没有 AlphaProof 加持，仅凭一个大模型循环外加编译器的硬核反馈，Agent A 就做到了。只不过，在解决某些难题时，它需要多烧一点算力。
研究团队将这一现象归因于两点：
Gemini 3.1 Pro 自身的基础能力已经足够强大。- Lean 编译器那种“实打实”的纠错反馈，对 AI 的引导作用远比人们预期的要大得多。
这个结果是否也在暗示着，随着基础模型能力的持续跃升，那些复杂的多工具组合系统可能不再是刚需？一个“大模型 + 专业校验工具”的精简闭环，或许就能搞定大多数曾被视作“人类智慧高地”的数学难题。
再者，这套方案的核心优势也直观地反映在了成本上——单题仅需几百美元。曾经，埃尔德什先生为这些难题逐一标定了悬赏金额，或许他唯独没有算到，最终打开这些尘封大门的，并非人类智慧的灵光一现，而是可复制、可规模化的通用算力。
论文地址： https://arxiv.org/abs/2605.22763v1
Github地址： https://github.com/google-deepmind/alphaproof-nexus-results
参考链接：
[1] https://x.com/pushmeet/status/2058936037754224998
[2] https://the-decoder.com/google-deepminds-alphaproof-nexus-solves-decades-old-math-problems-for-a-few-hundred-dollars/
技术的浪潮正以前所未有的速度重塑着基础科学的研究范式。如果你同样为这种“跨界”的力量感到震撼，不妨在云栈社区与更多极客和研究者一起，见证并参与这场变革。
发表于 4 小时前
|
查看: 4|
回复: 0
