56年没解开的题，AI全解了！谷歌DeepMind新成果登上Science主刊

　　新智元报道

　　谷歌的 AI 数学家，登上 Science 了！

　　论文里的主角，是 DeepMind 的 AlphaProof Nexus。9 项埃尔德什问题、44 项整数序列猜想，它都给出了证明。

　　其中两道老题，足足悬了 56 年。

　　Science 同期配发的评论，干脆就叫「研究数学的 AI 已经到来」。

　　在这里，数学家提出猜想，AI 自己找思路、写证明。它还能为优化算法找出新的参数设置，并证明为什么这样设有效。

　　这些新证明公开后，数学家又能接着简化、改进，继续做研究。

　　创造新知识这件事，人类开始和 AI 一起做了。

　　56 年的难题，终于解开了

　　先来看那两道悬了 56 年的老题。

　　它们是埃尔德什问题库第 12 号中的两个子问题，由埃尔德什和Sárközy 在 1970 年提出。

　　此后，Schoen、Baier、Elsholtz 等数学家接力研究，取得过不少进展，但这两问的完整证明，迟迟没有出现。

　　这两问，都围绕同一条选数规则展开——

　　挑出一些整数，其中任意一个数，都不能整除另外两个更大的数之和。比如2、3、5 就不能同时选，因为3+5=8，能被 2 整除。

　　第一问要求，选出的数要有无限多个；并且当N足够大时，从 1 到N里选出的数量，要始终不少于常数倍的√N。

　　这里的难点是，要避开整除关系，就得限制选数；可限制越多，剩下的数就越少。

　　Nexus 的做法是， 先按不同的数值区间分组选数，再分别处理组间和组内的关系。

　　对于不同组的数，它用中国剩余定理安排余数；在每组内部，则排除1、3、5 这类三项等差结构。这样，选出的数就能避开题目禁止的整除关系。

　　比如，让当前这组数都被某个奇质数整除，后面的数除以它都余1。这样，两个更大的数只要至少有一个来自后面的组，它们的和就会余 1 或余2，不可能被当前组里的数整除。

　　接下来还得保证数量。

　　对此，Nexus 会按照下一组起点对应的数量要求，提前选够当前组的数。

　　这样，即使N进入两组之间的空档，暂时没有新数加入，已经选出的数量也足够撑到下一组开始。

　　把这些组接起来，就得到了第一问要找的无限集合。

　　第二问则想知道，符合这条规则的数，最多能选出多少。

　　原来的猜想认为，可以找到一个小于 1 的固定指数，给所有这类集合划出数量上限，比如N的 0.9 次方或 0.99 次方。

　　AI 的反例表明，无论把指数定得多接近1，只要仍小于1，就能构造出最终一直超过这条线的集合。

　　至此，第 12 号问题的前两问，一正一反，都解决了！

　　这类成果，Nexus 一共拿下 9 项。

　　第 12 号问题的证明公开后，陶哲轩发现，前面那道「排除三项等差结构」的限制，其实可以删掉。

　　少了这道限制，构造就能简化。其他数学家也接着改进方案，让符合条件的数选得更多。

　　这样一来，AI 给出的证明，就成了同行可以继续做研究的起点。

　　陶哲轩在第 12 号问题讨论区指出，题目已有的条件就能排除 2a=b+c，因此不必额外限制三项等差结构

　　解题的关键，藏在循环里

　　从找到解题思路，到交出数学家能接着使用的完整证明，Nexus 靠的是 Gemini 和证明工具的一轮轮配合。

　　论文中的完整 Nexus 架构：证明生成、验证、草稿评估与搜索

　　在完整版的设计中，系统会让多个证明 Agent 共享草稿，由评审 Agent 比较哪份更清楚、更合理、更有新意，再决定优先沿哪条路线继续。

　　有的草稿虽然还没证完，却已经找到了关键构造，只差最后一个引理。于是，系统可以把更多计算用在这条有希望的路线上，接着补完。

　　遇到具体的子目标，Gemini 还可以调用 AlphaProof。大模型负责组织论证、选择怎么拆题，专门的证明器负责解决拆出来的步骤。

　　已经解决的子目标还会被缓存。因此，完全相同的目标再次出现时，系统能直接取回证明，接着往下做。

　　论文中的第 125 号题解题过程：Gemini 拆分目标，再调用 AlphaProof 完成局部证明

　　那么问题来了，解出这些难题，到底有多依赖上面这套复杂流程？为此，团队又做了一组对照测试。

　　他们去掉共享草稿的进化搜索，也不调用 AlphaProof，只保留 Gemini 3.1 Pro 与 Lean 的基本配合。

　　结果，拿那 9 道已经解出的埃尔德什问题重新测试，基础版经过多次独立尝试，也全部找到了证明。

　　相比之下，单独运行 AlphaProof，在同一组测试里一道也没解出。

　　也就是说，至少在这 9 道题上，通用大模型配合证明工具，已经能找到研究级的证明了。

　　从证明猜想，到改进算法

　　除了埃尔德什问题，Nexus 还尝试了整数序列在线百科 OEIS 中的 492 项猜想，为其中 44 项补上了证明。

　　研究人员经过人工核查，确认代码准确表达了原题，相关猜想此前也尚未被证明。

　　比如，从 1 到n里至少挑出一个整数，平均数恰好为整数的选法有多少种？数学家已经猜到n足够大时，这个数量会按什么公式增长，Nexus 补上了严格证明。

　　为减少题意在转换时走样，系统会先检查数列定义能否算出正确的前几项，再证明一般结论。

　　在这些数列问题里，AI 要做的是给已有猜想补上证明。

　　到了优化理论，任务又多了一步：它还得找出算法参数该怎么设。

　　Anchored GDA 处理的是这样一类问题。双方各自调整自己的变量，一方想把同一个目标值压低，另一方想把它抬高。

　　如果双方只顾着沿各自的方向调整，就可能来回震荡，迟迟找不到均衡。

　　因此，Anchored GDA 在每次更新时，会额外加上一项朝固定起点回拉的修正，帮助稳定整个过程。

　　但每步走多远、修正多强，都会影响收敛速度。于是，研究者把参数怎么设也交给 AI，让它连同证明一起找。

　　这项算法成果已于 4 月单独发表预印本，给出新的参数安排和收敛证明

　　AI 最终找到了一套新的参数设置，并证明：在论文规定的光滑、凸—凹等条件下，衡量收敛程度的「梯度范数平方」，可以达到O(1/t)的收敛保证。

　　t 就是迭代次数。这里的O(1/t)，表示这个指标的上界可以按迭代次数的倒数缩小。

　　此前悬而未决的，正是这种算法能否达到这一收敛速度。如今，严格证明有了。

　　至此，AI能做的事也多了一项：参与设计计算方法，并证明它为什么管用。

　　人类创造知识的方式，开始变了

　　论文发表后，DeepMind 的 Pushmeet Kohli 再次强调，推动数学进步，要让数学家做得更多。

　　想想看，如果这样的合作成为日常，一个数学家就能同时试更多想法。过去没精力细追的思路，如今也有机会一条条验下去。

　　而 AI 找到的新方法，还有可能被用来改进研究工具。工具更好，人和 AI 就有机会更快找到下一批答案。

　　一旦这样的发现接连出现，人类探索未知的速度，就有机会迎来一次大提速。

　　参考资料：

　　https://x.com/pushmeet/status/2108265638435119494

　　https://www.science.org/doi/10.1126/science.aej2213

　　https://www.science.org/doi/10.1126/science.ael6628

　　编辑：摩西