AI数学研究领域近期动态频繁。

OpenAI刚刚一次性发布了722份数学证明，引发数学界集体抵制，而谷歌DeepMind的数学成果则登上了《Science》。

一边是批量抛出待核验手稿，将校对负担转嫁给数学家；另一边是耐心等待数月，正经走完同行评审流程，接受了数学界的检验。

卡内基梅隆大学和南卡罗来纳大学的两位数学家，在同期《Science》上专门撰写评论：《用于数学研究的AI已经到来》。OpenAI那边还在为数学证明的发布方式争论不休，DeepMind这边已获得数学家的公开认可。

DeepMind此次的主角是AlphaProof Nexus，这是一套由Gemini驱动的AI数学证明Agent框架。它解决了9道埃尔德什开放问题，其中两道悬而未决长达56年。除这9道外，它还顺手证明了OEIS整数序列百科中的44个猜想、解决了一道搁置15年的代数几何难题，并改进了凸优化领域一个沿用已久的理论边界。

DeepMind也是《Science》的常客。这篇数学论文共有20位作者，其中Aja Huang是当年AlphaGo的核心研究员。

攻破56年悬赏难题

DeepMind从已有Lean形式化版本的问题中选出353道，交由AlphaProof Nexus尝试，最终成功解决9道。其中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的证明采用巧妙数学构造，将无限完全图的边映射成平面上的点，用多项式表达式编码坐标，再结合无穷组合数学相关结论完成证明。一个平面几何问题最终被转化为图论与组合数学问题解决。

除这三道外，还有六道问题分别涉及整除集构造、范德瓦尔登数间隙、西顿集孤立点、集合拆分密度等领域。

完成埃尔德什问题后，AlphaProof Nexus又前往OEIS整数序列百科，证明了44个开放猜想。它还涉足代数几何和凸优化领域，解决了代数几何中一道关于希尔伯特函数对数凹性的15年悬案，并改进了凸优化中一个锚定梯度下降法的理论边界。

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和进化搜索，也是此次批量探索开放问题时使用的主要配置。

按常理，功能越多应越强大。但DeepMind后续进行的对照实验发现，最简单的Agent A也能解出全部9道埃尔德什问题。没有进化算法，没有AlphaProof，仅靠LLM循环加编译器反馈的Agent A，只是在难题上更费钱。在#125和#138等困难问题上，完整版Agent的成本效率比基础版本高出约2至5倍。

综合计算，此次AlphaProof Nexus解一题的成本约在几百美元。整套Lean证明代码已公开，外界可直接查看。

埃尔德什生前曾为不少数学难题设立现金悬赏，鼓励全球数学家挑战。如今，除数学家的智慧外，算力也开始成为解开这些悬赏难题的关键。

本文来自微信公众号“量子位”，作者：关注前沿科技，36氪经授权发布。