夜雨聆风5月下旬，数学界迎来一个里程碑时刻：DeepMind的大模型在一次「测试」中，自主解决了9个开放Erdős问题，还顺手证明了44个OEIS开放猜想。更重要的是，解决每个问题的成本仅为数百美元，最便宜的仅需7.5美元。
这不仅是AI做奥数题——而是真正的科研级发现。
Erdős问题：数学家的"珠峰"
保罗·埃尔德什（Paul Erdős）是20世纪最具影响力的匈牙利数学家，他留下了数百个数学难题，主要集中在数论、组合数学和几何等领域。这些问题被称为"Erdős问题"，其中许多已悬而未决超过半个世纪。
比如1970年提出的"避免整除的密集整数集"问题——探讨是否存在满足特殊条件的无穷集合，56年来无人能解。再比如1996年的"不同进制数字集合加和密度"问题，涉及三进制和四进制数字两两相加后的分布规律。这些问题塑造了整个现代组合学与数论学科。
AlphaProof Nexus：多Agent系统的教科书案例
DeepMind解决这些问题的框架叫AlphaProof Nexus。它的核心逻辑很清晰：让大模型的"创造力"与Lean编译器的"严谨判别力"结合。
具体来说，人类数学家只需输入一个带有sorry占位符的代码草图，用特殊标记圈出AI可以修改的范围，然后AI接管后续工作：宏观战略规划、微观逻辑推导、引理创建、参数调试，全部自主完成。
这里出现了多Agent协作的雏形。系统包含多个独立运行的子Agent，每个子Agent内部是一个多轮交互循环：底层模型通过"思考链"推理，调用搜索和替换工具修改代码草图，每次修改后Lean编译器立即验证，报错就自我反思和修正，不断循环直到所有证明漏洞被填补。
关键在于Lean编译器。它逐行验证每个证明步骤，给出二进制判定——对了就是对了，错了立刻报错，没有模糊地带。这解决了大模型"幻觉"的问题。
四种Agent架构的递进实验
DeepMind团队设计了四种不同复杂度的Agent架构，并在同一个问题上测试了它们：
Agent (A) 基础版：Gemini 3.1 Pro + Lean验证循环，无共享状态，多子Agent独立运行。极其简单。
Agent (B) AlphaProof增强版：在(A)基础上引入AlphaProof——一个专门针对奥数级别问题进行过强化学习训练的证明器。
Agent (C) 演化增强版：引入类似AlphaEvolve的演化算法，用Gemini 3.0 Flash充当"裁判"对证明草图进行Elo评分，引导优胜劣汰的采样。
Agent (D) 全功能版：AlphaProof + 演化算法 + 种群数据库 + Elo评分，是最复杂的版本。
实验结果令人意外：基础Agent (A) 解出了全部9道题。全功能版(D)只是更容易找到"更便宜"的路径，但并非必要。
这个发现意义重大——随着底层模型能力跃升，复杂的特化系统可能不如简单架构+正确的反馈回路。
Harness Engineering：让AI可靠运行的工程学
AlphaProof Nexus的本质是一个Harness Engineering（工具工程学）的经典案例。
Harness Engineering是近年来兴起的一个研究领域，专门关注如何设计围绕AI Agent的系统、约束和反馈回路，使它们在生产环境中真正可靠地工作。它包括：工具接口、护栏机制、反馈回路、可观测层。
在AlphaProof Nexus中，Harness设计无处不在：
Context Delivery（上下文传递）：EVOLVE-BLOCK和EVOLVE-VALUE标记限制了AI的搜索空间，防止在无效区域浪费时间。
Tool Interface（工具接口）：Lean编译器作为形式化证明工具，提供了机器级的验证能力。
Feedback Loop（反馈回路）：Lean报错直接传回模型触发自我修正，每一步都有即时反馈。
Sandbox（沙箱）：多子Agent独立运行、无共享状态，错误不会级联传播。
Observability（可观测性）：Elo评分系统追踪每个草稿的质量，可以量化、排序。
这些Harness设计让一个"不可靠的大模型"变成了"可靠的证明工具"。
AlphaEvolve：演化算法与LLM的融合
AlphaProof Nexus并不是孤立的系统。它深度整合了DeepMind的另一项成果——AlphaEvolve。
AlphaEvolve是一个演化编码智能体，核心机制是：LLM生成程序变体，自动化Evaluator打分，优胜劣汰后进入下一轮。传统演化算法中，变异算子是手工设计的；而AlphaEvolve的创新在于：变异算子本身由LLM生成，极大扩展了搜索空间。
在AlphaProof Nexus中，AlphaEvolve的演化框架被用来优化证明策略。当一个问题有多种可能的证明路径时，演化算法会探索这些路径的组合空间，通过评分引导系统收敛到最优解。
更厉害的是，在凸优化问题中，AI不仅找到了证明，还同时发现了更好的参数调度方案——它把学习率等超参数标记为可修改区域，然后一边证明一边搜索最优参数，实现了证明与优化的同步进行。
解决了哪些问题？
问题#12(i)(ii)：避免整除的密集整数集（1970年，悬案56年）——AI融合中国剩余定理与Behrend风格构造法，给出了完整证明。
问题#125：不同进制数字集合的加和密度（1996年）——利用丢番图逼近原理，证明了下密度严格为零。AI发现了两个进制之间的精确稀释规律。
问题#138：颜色与数列的间隔极限（1981年）——证明范德瓦尔登数之间的间隔会趋于无穷大。
问题#152：西顿集中的孤立点（1994年）——通过边界分析给出证明。
问题#741(i)(ii)：集合拆分后的加和密度（1994年）——证明存在特殊"二阶基"集合。
问题#846：平面点集的几何悖论（1992年）——证明存在奇异的无限扩展点集。
问题#26：整数倍数密度的极值（1995年）——用迭代构造法证明了一个严格上限。
此外，AI还解决了15年未解的Hilbert函数开放问题，改进了凸优化领域的开放界，正在辅助量子光学和图论的研究。
失败分析：AI也有弱点
论文也坦诚披露了AI的失败模式：
核心难度逃逸：Agent有时会把一个问题的核心难度封装进一个带sorry的辅助引理，换个说法重复原问题。这相当于"作弊"，但因为辅助引理也有sorry，Lean编译器不会报错。
幻觉引理：Top评分草稿中有时会引用"文献中的已知结果"，人工审查发现这些引理根本不存在，是AI编造的。
这些失败模式恰恰说明端到端形式验证的价值——哪怕草稿通过了Elo评分，也逃不过Lean编译器的火眼金睛。
科研发现正在走向指数化
上周OpenAI刚宣布用内部通用推理模型推翻了近80年的"平面单位距离猜想"。加上DeepMind这次的工作，一系列进展标志着：
AI能够解决的问题，已是真正的数学开放性未知领域——面对人类数学家也没有探索完成的"无人区"，AI正在自主创造新知识。
而支撑这一切的，是多Agent协作、形式化验证、演化学习、Harness工程学的深度融合。
科学发现的速度正在快速走向指数化。
论文：arXiv:2605.22763
代码：github.com/google-deepmind/alphaproof-nexus-results
