AI Agent 正在推动研究级数学的进步。

日前，Google DeepMind 研究团队提出的 AlphaProof Nexus，首次在研究级数学问题上实现大规模突破。它成功解决了 9 个长期未解的 Erd ő s 开放问题，其中最早的一题已困扰学界 56 年。

AlphaProof Nexus 在其他数学问题上的表现同样亮眼：它证明了   44 个 OEIS 数学猜想，解决了悬置 15 年的纯 O- 序列对数凹性问题，并开始被用于组合数学、图论、优化理论、代数几何和量子光学等研究方向。

值得注意的是，这样的求解并不依赖极高成本：单题成本通常在 200 到 400 美元之间，最低仅为   7.5 美元。

相关研究论文已发表在预印本网站 arXiv 上，所有 Lean 形式化证明结果及部分自然语言证明也已在 GitHub 上公开。

论文链接：https://arxiv.org/abs/2605.22763v1https://arxiv.org/abs/2605.22763v1?ref=airadar.one

GitHub：https://github.com/google-deepmind/alphaproof-nexus-results

这些研究成果展示了 AI 辅助形式化证明搜索的强大能力，并揭示了实现这一目标的 Agent 设计原理。研究团队表示，数学的未来属于人机协作，交互式 AI 工具将进一步提升数学家的创造能力。

AlphaProof Nexus 是怎样设计的？

过去，大语言模型（LLM）虽然在数学推理上越来越出色，但论证时容易出现 " 幻觉 "，证明也难以直接验证真伪。AlphaProof Nexus 的特别之处，在于把大模型生成的证明过程放进 Lean 形式化系统中逐步验证。只有通过 Lean 检查，证明才算成立。

由于证明草稿都经过了 Lean 的形式化验证，即便 Agent 没能直接证明命题，这些形式化证明依然有助于帮助科学家理解数学问题，他们也不用从头再检查整套证明。

AlphaProof Nexus 的架构可以这么理解：Gemini 3.1 Pro 主要承担证明推理工作，负责生成并修改 Lean 证明草图；Lean 编译器则逐步检查证明，一旦发现错误，就会返回给 Agent 继续修正，如此反复，直到证明通过。此外，该 Agent 还配有验证器、进化式搜索和评分机制，帮助筛选更有希望的证明路径。

根据是否接入 AlphaProof，以及是否引入进化式搜索，研究团队将 AlphaProof Nexus 分成了 4 个版本：基础版 Agent（A）、AlphaProof 版 Agent（B）、进化版 Agent（C）、完整版 Agent（D）。

图｜AlphaProof Nexus 完整版 Agent 设计。

1. 基础版 Agent（A）

这是最基础的版本，多个 prover 子 Agent 同时工作，分别尝试同一道题的不同证明思路。每个 prover 都与 Gemini 3.1 Pro 进行多轮交互，修改 Lean 证明草图，再交给   Lean 编译器检查；如果出现报错，反馈会进入下一轮继续修正。若证明仍未完成，搜索就继续推进。

图｜基础 Agent（A）的伪代码

2.AlphaProof 版   Agent（B）

这一版本在基础流程上接入了   AlphaProof，它是 DeepMind 此前面向奥数级 Lean 证明训练的强化学习系统，可以用来处理证明草图中尚未完成的局部子目标。prover 会把这些子目标交给 AlphaProof；若求解成功，结果就直接写回草图；若失败或得到反证，相关反馈则回到后续推理过程中。

3. 进化版   Agent（C）

这一版本引入了进化式搜索。在前两个版本中，各个 prover 都是从同一初始草图独立搜索，彼此之间不共享结果。Agent（C）则引入了共享草图库，每个 prover 都可以在已有草图基础上继续修改，并把新版本放回库中。此外，评分模块会根据草图的可行性、清晰度和新颖性给出 Elo 分数，Agent 再优先沿着高分草图继续搜索，从中筛出更有希望的证明路径。

4. 完整版 Agent（D）

这是 AlphaProof Nexus 用于大规模探索开放问题的核心版本。它结合了 AlphaProof 的局部证明能力，并引入基于共享草图库的进化式搜索机制。每一轮，Agent 都会从草图库中挑选更有希望的证明草图，交由 Gemini 3.1 Pro 继续完善；对于此前已经解决过的问题，则可以直接复用已有结果，避免重复求解。

图｜完整版 Agent（D）主要组件的伪代码。

AlphaProof Nexus 的能力怎么样？

1.Erd ő s 问题：353 题中证明 9 题

研究团队在已形式化的 353 道 Erd ő s 开放问题上进行了系统评测，最终攻克其中 9 题，并全部通过 Lean 验证。

图｜完整版 Agent 自主解决的 ErdosProblems 仓库中的开放问题。

其中，  问题是一个代表性案例。这个问题研究的是一个特殊和集：一类数的三进制表示只含 0 和 1，另一类数的四进制表示也只含 0 和 1；将两类数两两相加，就得到这个和集。自 1996 年提出以来，学界一直不清楚它的下密度是否为正。AlphaProof Nexus 最终给出了否定答案，证明该和集的下密度为 0，并在 Lean 中完成了形式化证明。

此外，其余几道题的证明路径也各不相同，分别涉及分块构造、中国剩余定理、无三项等差集、图着色和密度界估计等多种方法。

AlphaProof Nexus 还帮助团队发现了原题中的表述歧义。以    和   ( i ) 问题为例，题目对 "density" 的含义并不明确。团队核对原题后，澄清了相关定义并据此重写了形式化表述，顺利完成了证明。

2.OEIS：492 个猜想中证明 44 个

除 Erd ő s 问题外，研究团队还从 OEIS 中筛选并形式化了 492 条适合自动定理证明的开放猜想，最终证明了其中 44 条此前未被解决的命题。经人工复核，这些结果对应的命题形式化准确无误。研究团队指出，这表明形式化证明搜索已不再局限于单题，而具备在较大规模问题集上系统运行的可行性。

3. 已走向真实研究

除了在开放问题集上进行系统评测，AlphaProof Nexus 也已被用于真实数学研究。在代数几何中，它解决了 4 道开放题中的 2 道，其中一题是悬置约 15 年的希尔伯特函数对数凹性问题；在优化理论中，它还为一类梯度下降 - 上升算法给出了更强的收敛速率证明，并改进了已有理论边界。

AlphaProof Nexus 也已被用于图论、加法组合学和量子光学等方向，并在这些领域取得了具体成果，包括证明部分问题、澄清并证伪部分问题，以及解决多条猜想。

4. 简单版本也有较强的解题能力

研究团队比较了 4 个版本的 Agent 在 Erd ő s 问题上的表现。结果显示，最简单的基础 Agent 也解出了完整版 Agent 攻克的那 9 道 Erd ő s 问题，只是在较难问题上成本更高。研究团队指出，随着底层大模型能力提升，较简单的 Agentic loop 也开始在研究级数学任务中展现出更强能力；不过在 Erd ő s  、  这类更困难的问题上，全功能 Agent 目前仍具有更高的效率。

不足与未来方向

尽管 AlphaProof Nexus 已取得不少突破性成果，研究团队对其能力边界和实际成本的判断仍相当克制。

目前，AlphaProof Nexus 的成功主要集中在组合数学、凸优化和数论等方向。这些领域的 Lean 数学库相对成熟，问题本身也更容易被拆解和形式化。即便如此，大部分 Erd ő s 问题仍超出该 Agent 的能力范围。研究团队认为，未来要推进到更广泛的数学领域，仍有赖于底层模型能力提升、Lean 数学库持续扩展，以及搜索机制的进一步优化。

研究团队同时指出，该 Agent 仍继承了底层大模型的偏差，搜索过程也存在较高方差。未来，如何降低偏差与波动、提升系统稳定性，仍是重要的发展方向。

与此同时，求解成功后的单题推理成本，并不等于完整发现过程的真实成本。真正解题之前，研究团队先用完整版 Agent 对   353 道 Erd ő s 问题逐一尝试求解，这一步就需要消耗大量算力。未来，除了提高解题能力，还需要进一步压低大规模筛题和搜索的整体成本。

更多技术细节，详见原论文。

作者：夏千斯

如需转载或投稿，请直接在本文章评论区内留言