AlphaProof Nexus 将大语言模型驱动的证明生成与机器验证相结合，攻克了数十年来令数学家束手无策的数学研究难题。

谷歌DeepMind的新框架AlphaProof Nexus已自主解决了它尝试的353个开放埃尔德什问题中的9个，其中包括两个56年来无人解答的问题。

该系统还证明了整数序列在线百科全书（OEIS）中492个开放猜想中的44个，解决了一个关于代数几何中希尔伯特函数的15年悬而未决的问题，并改进了凸优化中的一个已知界限。根据研究论文，每个问题的推理成本仅为几百美元。

与OpenAI近期解决方案那种（可能）纯粹的自然语言方法不同，AlphaProof Nexus中的底层语言模型——本例中为Gemini 3.1 Pro——无需独自承担整个逻辑链条。

相反，它用Lean的形式化语言生成证明步骤，编译器会逐一检查。错误信息会直接反馈到下一次尝试中。这样一来，大语言模型便获得了符号反馈的支撑，这道安全网弥补了语言模型在逻辑推理方面众所周知的弱点。人类仅在最后阶段介入以检查结果。

四个智能体，一个令人惊讶的结果

该系统由四个复杂度递增的智能体变体组成。最简单的智能体（A）部署了在Gemini 3.1 Pro上循环运行的独立子智能体：语言模型生成证明步骤，Lean编译器进行检查，错误信息反馈到下一次尝试中。

智能体（B）增加了对AlphaProof的查询，这是谷歌基于强化学习的奥数解题系统，能够填补缺失的证明片段。智能体（C）引入了进化组件。受AlphaEvolve启发，子智能体共享一个共同的证明草图种群。基于Gemini 3.0 Flash构建的评分智能体对这些草图的合理性和新颖性进行评分，然后使用Elo系统进行排名。功能完备的智能体（D）结合了所有这些能力。

智能体 (D) 被用于解决 Erdős 问题。但一项事后分析带来了一个意外发现：最简单的智能体 (A)，仅使用大语言模型和编译器反馈，也能证明所有九个已解决的 Erdős 问题，尽管在最难的题目上成本更高。

研究人员将简单智能体的成功归因于两个因素：底层语言模型的快速改进，以及“编译器反馈在约束大语言模型推理方面的强大作用”。目前，功能完备的智能体在最困难的任务上仍占优势，但随着大语言模型能力的提升，这一优势可能会缩小。研究人员认为这指向一个更广泛的趋势，他们将其描述为“随着大语言模型能力增强，从专门的训练系统向简单智能体循环的持续转变”。

即使没有完整证明也有用

该系统的成功主要集中在组合数学、凸优化和数论等领域，在这些领域，Lean 的数学库 Mathlib 已经成熟，并且问题可以分解为可管理的子目标。研究人员写道，大多数 Erdős 问题仍然无法解决，“更不用说那些需要大量新理论的问题了”。这些智能体也继承了底层语言模型不可靠的特性。

尽管如此，他们看到了超越已解决问题之外的价值。使用该系统的数学家报告说，即使是失败的证明尝试也加深了他们对问题的理解，或者正如作者所说，“由人工智能驱动的形式化证明搜索不仅可以用于解决问题，还可以加深人类的理解。”

由于证明草稿是形式化的，专家可以专注于未解决的子目标，而无需从头重新检查整个论证。这些智能体在发现文献中形式化错误方面也表现出色。作者写道：“形式化验证可以作为一道过滤器，用于判断哪些证明值得人工审阅。”

根据论文，该系统已被用于正在进行的量子光学和图论研究中。所有 Lean 证明和选定的自然语言证明均已在 GitHub 上公开。

Erdős 问题成为人工智能数学的基准

OpenAI 近期使用一款专有推理模型推翻了埃尔德什的单位距离猜想。菲尔兹奖得主蒂莫西·高尔斯称其为“AI 数学领域的一座里程碑”。在此之前，GPT-5.2 Pro 帮助解决了埃尔德什问题 #281，陶哲轩称该案例是“或许最明确的一个实例”，证明了大语言模型解决开放数学问题的能力。此后，GPT-5.4 又解决了另一个埃尔德什问题。

从某些方面看，这些成果比 DeepMind 的方法更令人印象深刻。该语言模型必须通过自然语言承载整个逻辑链条，而没有 Lean 编译器来检查每一步。AlphaProof Nexus 更具系统性和可扩展性，但它追求的是不同目标：构建一个用于日常数学研究的可靠 AI 工具。当然，OpenAI 也可以将 Lean 集成到他们的框架中，但关键在于，这更多是为了测试原始大语言模型的能力。

不过，陶哲轩此前曾警告不要过度解读这些头条新闻。AI 在埃尔德什问题上的实际成功率仅为百分之一到二，且集中在较容易的问题上。谷歌的系统在 353 个问题中仅破解了 9 个。这与陶哲轩提出的 2% 门槛几乎完全吻合。