近日，谷歌DeepMind团队发布了全新AI数学智能体AlphaProof Nexus，一举解决了9道悬而未决的埃尔德什开放问题（Erdős problems），其中最古老的问题已搁置56年。所有证明均通过Lean编译器进行了形式化验证，确保数学上的严谨性。该成果标志着AI在开放式数学研究领域迈出了实质性一步。
除了9道埃尔德什问题，该系统还证明了OEIS整数序列百科中的44个开放猜想，解决了一道搁置15年的代数几何难题（希尔伯特函数的对数凹性），并改进了凸优化领域中锚定梯度下降法的一个理论边界。整套证明代码已开源在GitHub上。研究共有20位作者，论文以arXiv预印本形式公开。
三道典型难题的破解路径
无限整数集的三元整除约束
第一道题要求构造一个无限大的整数集合，满足：任意取三个不同的数a、b、c，a永远不能整除b加c的和；同时该集合在自然数中保持一定密度（下密度非零）。该问题自1970年提出以来，人类仅能给出局部构造，始终无法获得完整的无限集。AI的解法则利用中国剩余定理将大问题拆解为多个独立区块，每个区块内部通过三项等差数列的回避集来满足约束，最后将各区块拼接成完整的无限集。
数字集合加法的密度判断
第二个问题涉及两个集合：集合A由“三进制下只由数字0和1组成的整数”构成，集合B由“四进制下只由0和1组成的整数”构成。将两个集合中的数字两两相加，得到新集合，问题是该新集合在自然数中的下密度是否为正。该问题自1996年提出后悬而未知。AI利用log₄除以log₃是无理数的性质，说明3的幂次和4的幂次可以任意精度彼此逼近，进而构造归纳性稀疏化论证，使密度以0.99的比率逐步衰减直到归零，最终证明下密度确实为零。
平面点集的全局不可拆分性
第三道是平面几何题：证明存在一个无限扩展的平面点集，使得任意有限子集都包含大量不共线的点（即任意有限子集的大部分点不共线），但整个集合无法被拆分成有限个“绝对无三点共线”的子集。AI将完全图的每条边映射到平面上的一个点，用二次多项式编码坐标，并引入无穷Ramsey定理，把一个几何问题转化为图论和逻辑语言，完成了证明。
架构核心：形式化验证与多Agent协同
AlphaProof Nexus的架构核心是“编写证明代码 + 编译器验证”的反馈循环。系统内置三种不同类型的智能体（Agent），分别探索不同的解题策略：
Agent A：最基础的方案。仅依靠大语言模型Gemini 3.1 Pro梳理解题思路，编写证明代码（Lean语言），然后交给编译器核验。一旦编译器报错，错误信息会传回模型，模型修改代码并重试，直到验证通过。全部过程无需额外工具，仅靠LLM+编译器循环。
Agent B：在Agent A的基础上，当遇到某个小步骤反复卡住时，可调用AlphaProof（DeepMind此前专为奥数级别题目训练的强化学习证明工具）进行树搜索，攻击局部难点。
Agent C：多个子Agent共享一个证明草图“种群”。每个子模块产出不同的证明草稿，由另一个模型从合理性、清晰度、新颖性三个维度打分（Elo评分系统）。高分草稿相互组合衍生新解法，低分草稿被淘汰，整个种群在证明空间中进行进化搜索。
出人意料的是，在本次大规模评估中，表现最佳的并非结构最复杂的Agent C，而是最简单的Agent A——仅靠LLM循环加编译器反馈，就完成了所有9道题的证明。Agent B和Agent C在部分难题上虽有一定帮助，但整体效率并不优于A。这一结果暗示，随着大模型能力持续提升，复杂的多工具组合系统可能不再是解决数学难题的必需条件。单题成本仅需几百美元（约合人民币数千元）。
成本与验证的突破
菲尔兹奖得主陶哲轩此前曾指出，AI目前解决埃尔德什问题的实际成功率大约在1-2%。本次系统在353道题的测试集中解开了9道，比例恰好落在该估算范围内。所有证明代码均经过Lean编译器的形式化验证，不存在大模型常见的“幻觉”问题，人工程序员也确认了解法的正确性。
埃尔德什生前曾为这些难题设置了悬赏，鼓励后来者破解。如今，解开这些谜题的不仅有人类智慧，还有经过大规模算力训练的AI。值得注意的是，DeepMind已将全部证明代码开源，供全球数学研究社区检验与复用。
论文地址：https://arxiv.org/abs/2605.22763v1
Github地址：https://github.com/google-deepmind/alphaproof-nexus-results
本文参考来源：量子位
微信扫描下方的二维码阅读本文
