AlphaProof Nexus 以低成本攻克开放数学难题
The Decoder··作者 Matthias Bastian
关键信息
该系统使用 Gemini 3.1 Pro 生成 Lean 证明步骤，并由 Lean 编译器在步骤失败时提供即时反馈。DeepMind 描述了四种代理变体，事后分析还发现，最简单的“LLM 加编译器反馈”循环也能解决这 9 个 Erdős 问题，只是在最难的问题上成本更高。
资讯摘要
Google DeepMind 的 AlphaProof Nexus 被描述为一个把语言模型生成证明与 Lean 形式化验证结合起来的框架。报道称，它在尝试的 353 个开放 Erdős 问题中，自动解决了 9 个，其中包括两个已经悬而未决 56 年的问题。它还证明了《整数数列在线百科全书》（OEIS）中的 492 个开放猜想里的 44 个，解决了一个关于代数几何中 Hilbert 函数的 15 年旧问题，并改进了一个凸优化中的已知界。报道提到，每个问题的推理成本只有几百美元。其核心机制是由 Gemini 3.1 Pro 在 Lean 中提出证明步骤，然后由编译器检查这些步骤，并把错误信息反馈给下一轮尝试。
DeepMind 认为，这种方式把模型推理锚定在符号反馈上，减少了语言模型独自承担完整逻辑链条的压力。该系统包含四种复杂度逐步提升的代理，最先进的版本结合了独立证明搜索、AlphaProof 式的缺失片段补全，以及进化式排名循环。不过，事后分析发现，最简单的代理只靠 LLM 和编译器反馈，也能证明这 9 个 Erdős 问题，这说明模型能力提升和编译器反馈可能才是主要驱动力。研究人员同时强调，大多数 Erdős 问题仍然没有被解决，尤其是那些需要大量新理论的问题，而且该方法仍受底层语言模型可靠性的限制。即便如此，他们认为这种方法的价值不只在于完成证明，还可能帮助数学家探索方向并支持研究流程。
资讯正文
Google DeepMind 的 AlphaProof Nexus 只花几百美元就解决了数十年前的数学难题
要点
- Google DeepMind 开发了 AlphaProof Nexus，这是一个框架，能够自主解决 353 个开放的 Erdős 数学问题中的 9 个，以及其他复杂猜想；按每个问题计算，推理成本仅为几百美元。
- 该系统依赖 Gemini 3.1 Pro 语言模型在 Lean 中生成证明步骤。Lean 是一种用于数学验证的形式化编程语言，从而实现严谨且可机器检查的解答。
- 尽管绝大多数 Erdős 问题仍超出了 AI 的能力范围，DeepMind 研究人员仍认为，该系统是支持数学研究的宝贵工具。
AlphaProof Nexus 将 LLM 驱动的证明生成与机器验证结合起来，攻克了困扰数学家数十年的数学研究问题。
Google DeepMind 的新框架 AlphaProof Nexus 在其尝试的 353 个开放 Erdős 问题中，已自主解决了 9 个，其中包括两个已悬而未决 56 年的问题。
该系统还证明了《整数数列在线百科全书》（OEIS）中的 492 个开放猜想里的 44 个，解决了一个关于代数几何中 Hilbert 函数的 15 年旧问题，并改进了一个已知的凸优化界限。根据研究论文，其推理成本每个问题仅为几百美元。
不同于 OpenAI 最近那种（可能）纯自然语言式的解法，AlphaProof Nexus 背后的语言模型——在这里是 Gemini 3.1 Pro——不必独自承担完整的逻辑链条。
相反，它使用 Lean 的形式化语言生成证明步骤，由编译器逐步检查每一步。错误信息会直接反馈到下一次尝试中。这样一来，LLM 就通过符号反馈得到了锚定，这种安全网弥补了语言模型在逻辑推理方面众所周知的弱点。人类只会在最后阶段介入，检查结果。
四个代理，一个出人意料的结果
该系统由四种复杂度逐步提升的代理变体组成。最简单的 Agent (A) 通过循环运行基于 Gemini 3.1 Pro 的独立子代理：语言模型生成证明步骤，Lean 编译器检查这些步骤，错误信息再反馈到下一次尝试中。
Agent (B) 额外查询 AlphaProof——Google 基于强化学习的奥赛数学系统，它可以补全缺失的证明片段。Agent (C) 引入了进化式组件。受 AlphaEvolve 启发，子代理共享一个共同的证明草图种群。基于 Gemini 3.0 Flash 构建的评分代理会根据可信度和新颖性对这些草图打分，然后使用 Elo 系统进行排序。功能最完整的 Agent (D) 将上述所有能力结合在一起。
Erdős 问题使用的是 Agent (D)。但事后分析带来了一个惊喜：最简单的 Agent (A)——只使用 LLM 和编译器反馈——也能证明全部 9 个已解决的 Erdős 问题，不过在最难的题目上成本更高。
研究人员将这个简单代理的成功归因于两个因素：底层语言模型的快速改进，以及“编译器反馈在让 LLM 推理落地方面的力量”。目前，功能完整的代理在最难的任务上仍占有优势，但随着 LLM 变得更强，这一领先优势可能会缩小。研究人员表示，这指向一个更广泛的趋势，他们将其描述为“随着 LLM 能力不断增强，从专门训练的系统向简单的代理式循环持续转变”。
即使没有完整证明也有用
该系统的成功主要集中在组合数学、凸优化和数论等领域，在这些领域里，Lean 的数学库 Mathlib 已经相当成熟，而且问题可以分解为可管理的子目标。研究人员写道，大多数 Erdős 问题仍然难以触及，“更不用说那些需要大量新理论的问题了”。这些代理还继承了底层语言模型的不可靠性。
尽管如此，研究人员认为其价值并不局限于已解决的问题。与系统合作的数学家表示，即便证明尝试最终失败，也加深了他们对问题的理解；正如作者所说，“AI 驱动的形式化证明搜索不仅可以用于解决问题，也可以加深人类理解。”
由于这些证明草图是形式化的，专家们可以把注意力集中在尚未解决的子目标上，而不必从头重新核对整个论证。事实证明，这些代理在发现文献中有缺陷的形式化方面也很有效。作者写道：“形式化验证可以作为一种过滤器，用于判断哪些证明值得人类审查。”
论文称，该系统已经被用于量子光学和图论的持续研究中。所有 Lean 证明以及选定的自然语言证明都已在 GitHub 上公开。
Erdős 问题成为 AI 数学的基准
OpenAI 最近使用一种专有推理模型推翻了 Erdős 的单位距离猜想。菲尔兹奖得主 Tim Gowers 称这“是 AI 数学领域的一个里程碑”。在此之前，GPT-5.2 Pro 帮助解决了 Erdős 问题 #281，Terence Tao 称这一案例“也许是 LLM 解决开放数学问题最无可争议的实例”。随后，GPT-5.4 又解决了另一个 Erdős 问题。
从某种程度上说，这些结果比 Deepmind 的方法更令人印象深刻。语言模型必须在没有 Lean 编译器逐步检查的情况下，通过自然语言承担整个逻辑链条。AlphaProof Nexus 更加系统化，也更具可扩展性，但它瞄准的是一个不同的目标：打造一个适用于日常数学研究的可靠 AI 工具。当然，OpenAI 也可以把 Lean 集成到他们的脚手架中，但那里的重点更多是测试原始 LLM 能力。
不过，Tao 过去曾警告不要对这些头条过度解读。AI 在 Erdős 问题上的实际成功率只有 1% 到 2%，而且主要集中在较容易的任务上。谷歌的系统只解出了 353 道题中的 9 道。这与 Tao 提出的 2% 门槛几乎完全一致。
来源与参考
收录于 2026-05-26