谷歌 AI 框架 AlphaProof Nexus 攻克 2 道悬置 56 年数学难题

5 月 26 日消息，谷歌 DeepMind 最新推出 AlphaProof Nexus，结合大语言模型（LLM）生成证明与 Lean 形式化验证，在 353 个开放的 Erdős 问题中自主解决 9 个，并解开 2 个悬而未决 56 年的问题。

注：Lean 是一种形式化证明语言和证明助手系统。研究者可以把数学命题、定义和证明步骤写成严格可检查的代码，编译器会逐步判断每一步是否合法。

Erdős 问题（Erdős problems）是由 20 世纪最高产的匈牙利数学家保罗 · 埃尔德什（Paul Erdős）提出的一系列数学猜想和问题，涵盖组合数学、数论、图论和几何等领域。

根据谷歌论文内容，AlphaProof Nexus 在 353 个开放的 Erdős 问题中解决了 9 个，其中 2 个问题已悬而未决 56 年。

AlphaProof Nexus 还在 OEIS（整数序列在线百科全书）的 492 个开放猜想中证明了 44 个，解决 1 个存在 15 年的 Hilbert 函数问题，并改进了凸优化中的已知界限。每个问题的推理成本只要数百美元。

在架构方面，AlphaProof Nexus 由 4 个复杂度递增的 AI 智能体组成：

Agent A 只依赖 Gemini 3.1 Pro 与 Lean 编译器循环交互。

Agent B 接入 AlphaProof，补全缺失证明片段。

Agent C 加入类似 AlphaEvolve 的进化机制，让多个证明草稿共享、评分、排序。

功能最完整的 Agent D 则整合了上述能力。

原本用于攻克 Erdős 问题的是 Agent D，但研究者发现，最简单的 Agent A 其实也能证明这 9 个已解问题，只是在最难题目上花费更高。

研究团队认为，这反映出 2 点变化：底层模型能力持续提升，以及编译器反馈对 LLM 推理的“锚定”作用越来越强。

附上参考地址

Advancing Mathematics Research with AI-Driven Formal Proof Search

AlphaProof Nexus 结果