AI数学圈最近是真热闹。
OpenAI前脚一口气甩出722份数学证明，把核对重担甩给整个数学界，后脚谷歌DeepMind的数学研究就登上了《Science》。一个批量抛出待核验手稿，一个老老实实等了几个月，正儿八经走完了同行评审。
同一周，两种做研究的姿态，高下立判。
两种发布方式，两种命运
10月6日，OpenAI在GitHub上发布了722份AI生成的数学手稿，涵盖数论、几何、代数、理论计算机等领域的372组结果。声势浩大，但只有162份的主要结果经过计算机验证。第二天，OpenAI撤回了3份手稿：一个符号错误推翻了一个核心论证，进而影响了依赖它的两篇论文；另有14份论文被修订，13份论文更新了引用关系。
菲尔兹奖得主、加州大学洛杉矶分校数学教授陶哲轩转发了人类数学协会（Association for Human Mathematics）的抵制声明。该协会要求数学家停止与OpenAI合作，成员必须承诺不为商业人工智能公司提供技术劳动、数学知识、咨询或宣传服务，也不发表由人工智能模型生成的数学文本。
而DeepMind走的是另一条路。这套名为AlphaProof Nexus的AI数学证明系统，早在2026年5月21日就把预印本挂上了arXiv，然后交给期刊同行评审。几个月后，论文正式发表于《Science》，DOI为10.1126/science.aej2213。
卡内基梅隆大学和南卡罗来纳大学的两位数学家，专门在同期《Science》上写了篇评论：《用于数学研究的AI已经到来》。OpenAI那边还在为发布方式吵得不可开交，DeepMind这边已经收获了数学家的公开肯定。
攻破56年悬赏难题
AlphaProof Nexus解决的第一批战果，分量不轻。
论文称，DeepMind从已有Lean形式化版本的问题中选出了353道埃尔德什开放问题，交给AlphaProof Nexus尝试，最终成功解决了9道。其中两道题足足悬了56年。
Erdős #12在1970年提出，至今悬而未决56年。这题问的是，能不能找出一个无限大的整数集合，让集合里的数字满足严格的整除限制，同时还得保持足够大的规模？具体来说，任意选取其中三个满足条件的整数，较小的那个不能整除另外两个更大整数的和，而且这个集合还不能太稀疏。从1970年起，就没人能给出这个集合的完整构造，各种局部进展有，但始终拼不成一个整体解。
这次AlphaProof Nexus的解法是分块构造。先把要构造的无限集合拆成一个个整数区块，然后利用中国剩余定理，结合避免三项等差数列的集合性质，让各个区块满足局部整除条件，最后再把所有区块拼回一个完整的无限集。
Erdős #125，1996年提出，30年没有定论。想象两个数字集合：第一个集合里全是“在三进制下只由数字0和1组成的整数”，第二个集合里全是“在四进制下只由数字0和1组成的整数”，把这两个集合里所有数字两两相加，得到一个新集合。问：这个新集合里的数字在自然数中出现的频率，也就是数学上说的下密度，是不是正的？
直觉上你可能会觉得，两种集合包含的数字本来就不算很多，加起来应该也挺稀疏的。但稀疏到什么程度？是彻底稀到密度归零，还是多少保持一点正密度？这中间的差别非常微妙，1996年提出后一直没定论。AlphaProof Nexus给出的答案是：下密度为零。
证明的关键，在于log₄/log₃是无理数。这意味着3的幂和4的幂可以在适当尺度下任意接近。利用这一点，AI构造了一个归纳性稀疏化论证：不断找到两个几乎对齐的尺度，让集合密度一步步衰减，直到彻底归零。
Erdős #846，1992年提出，卡了人类34年。这是一个关于平面点集的问题：能不能构造一个无限大的平面点集，让它具有一种很奇怪的性质，从中任意取出有限个点，都能找到一个规模足够大的子集，使其中没有三点共线；但如果试图把整个无限点集拆成有限个完全没有三点共线的集合，却办不到。简单理解，就是局部看着挺规矩，整体却怎么也拆不干净。
AlphaProof Nexus的证明采用了一种巧妙的数学构造。它把无限完全图的边映射成平面上的点，用多项式表达式编码坐标，再结合无穷组合数学中的相关结论，完成证明。一个平面几何问题，最后被转成图论与组合数学问题来解决。
除了这三道，还有六道分别在整除集构造、范德瓦尔登数间隙、西顿集孤立点、集合拆分密度等领域。
做完埃尔德什问题，它又跑去OEIS整数序列百科里证明了44个开放猜想。连代数几何和凸优化也没落下：在代数几何那边解决了一道希尔伯特函数对数凹性的15年悬案，在凸优化那边改进了一个锚定梯度下降法的理论边界。
这篇论文共有20位作者，其中的Aja Huang，也是当年AlphaGo的核心研究员。
Gemini写证明，Lean判卷
AlphaProof Nexus的核心工作方式很清晰：Gemini 3.1 Pro写证明，Lean检查，报错反馈给Gemini，修改证明，再检查，直到证明全部通过。
围绕这套流程，DeepMind设计了四种Agent配置。
最简单的Agent A，就是多个独立的子Agent同时尝试证明。每个子Agent都通过Gemini生成Lean代码，再根据编译器反馈不断修改。全程没有额外辅助工具，纯靠写代码加查错循环。Agent B增加了AlphaProof，这是DeepMind此前开发的专门数学证明系统，遇到难以解决的子问题时，Agent可以调用AlphaProof进行针对性搜索。Agent C引入进化搜索，多个Agent把不同的证明草稿放进共享数据库，再由基于Gemini 3.0 Flash的评分Agent比较草稿的合理性、清晰度和新颖性，系统把比较结果汇总成Elo评分，再据此挑选值得继续探索的证明路线。Agent D则是完整版，把AlphaProof和进化搜索都整合进来，也是这次批量探索开放问题时使用的主要配置。
按理说，功能越多，应该越厉害。但论文里的一组对照实验发现，最简单的Agent A，居然也能解出全部9道埃尔德什问题。没有进化算法，没有AlphaProof，就一个LLM循环加编译器反馈，只是在难题上更费钱一点。在#125和#138等困难问题上，完整版Agent的成本效率比基础版本高出约2至5倍。
综合算下来，AlphaProof Nexus解一题的成本大概在数百美元。这次的整套Lean证明代码已经公开，外界可以直接查看。
说起来，埃尔德什生前还曾为不少数学难题设立现金悬赏，鼓励世界各地的数学家来挑战。如今，数学家的智慧之外，算力也开始成为解开这些悬赏难题的关键。
数学研究的范式正在被重写
把两件事放在一起看，意味就出来了。
OpenAI的做法，本质上是一场力量展示。722份手稿一次性抛出来，潜台词是，我产出的速度已经远超你们核验的速度，你们自己看着办。这在工程上或许高效，在学术共同体眼里却是另一种信号：它把验证成本外部化给了整个领域。
DeepMind的选择则相反。预印本挂出去，等几个月同行评审，接受数学家的检验，再正式发表。速度慢，但每一步都踩在学术规范上。
数学家用脚投票。一边是抵制声明，一边是同期评论《用于数学研究的AI已经到来》。同样是AI做数学，待遇天差地别。
这背后其实是一个更根本的问题：当AI产出知识的速度开始超过人类消化的速度，数学这门最讲究严谨的学科，该靠什么来守住底线？
Lean这样的形式化验证工具给出了一种答案。它不关心证明是谁写的，只关心每一步推理是否经得起机器检查。DeepMind的整个闭环，Gemini写、Lean判、错了再改，正是把信任从相信某个机构，转移到了相信可复现的验证流程上。
OpenAI那722份手稿里，只有162份的主要结果经过计算机验证，剩下的要靠人眼去读。而DeepMind交出的，是整套可以公开检查的Lean证明代码。
一个把不确定性留给世界，一个把确定性写进代码。
当OpenAI把722份手稿甩给世界时，它赌的是速度；当DeepMind把论文交给同行评审时，它赌的是信任。在数学这门最讲究严谨的学科里，最后赢的往往不是跑得最快的，而是最守规矩的。
AI已经会做数学了，但数学之所以还是数学，不在于答案来得多快，而在于每一步都经得起追问。
快报