新智元报道
的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
编辑：摩西
