AlphaProof Nexus 深度解读：当 AI 不再猜测，而是以形式化为剑

论文：AlphaProof Nexus: A System for Autonomous Mathematical Discovery
作者：谷歌 DeepMind 团队
arXiv：2605.22763

问题的本质：数学证明与 AI 幻觉的正面冲突

数学家有一个古老的噩梦：证明看起来对了，但其实暗藏漏洞。AI 把这个噩梦放大了百倍。

大语言模型可以写出看似严密的数学论证，字句通顺、符号工整，但里面可能藏着微妙的逻辑断裂。人类审稿人需要逐行核查，而顶尖数学家也未必能在几小时内发现所有问题。

AlphaProof Nexus 的破局思路极其直接：不让人类审稿，让编译器审稿。

核心机制：LLM 的直觉 + Lean 的铁面

系统由两个核心组件咬合而成：

Gemini 3.1 Pro —— 负责提出证明思路。它像一位直觉敏锐的数学家，能从已知定理中嗅出潜在路径，生成证明草稿。

Lean 4 编译器 —— 负责严格验证每一步。它不读「氛围」，只认逻辑。任何一步推导不符合形式化规则，立即报错，证明被拒绝。

这个循环反复运行：Gemini 生成 → Lean 验证 → 出错则反馈错误信息 → Gemini 修正 → 再次验证。直到编译器通过，证明才被接受。

关键洞察：编译器反馈才是系统的真正灵魂。 研究者做了消解实验——去掉进化算法、去掉 AlphaProof 辅助，仅保留「Gemini + Lean 基础循环」，最简单的 Agent A 依然能证明那 9 道 Erdős 难题。其他模块是锦上添花，编译器反馈循环才是雪中送炭。

四级智能体架构：从简单到复杂

一个反直觉的发现：最难题目确实需要 Agent D，但那 9 道已解的 Erdős 问题，Agent A 也能搞定——只是成本更高。这说明 核心机制足够强大，复杂架构是效率优化而非必要前提。

战绩：56 年悬案告破

Erdős 问题（353 个开放问题）：

• 自主解决 9 个
• 其中 2 个悬而未决 56 年（自 1970 年提出）

OEIS 猜想（492 个开放猜想）：

• 证明 44 个

其他突破：

• 解决 1 个存在 15 年的 Hilbert 函数问题
• 改进凸优化中的已知界限

成本：每道题推理花费 数百美元

为什么这件事非同寻常

1. 100% 零误差

每个证明都经过 Lean 编译器的形式化验证。不存在「看起来对其实错了」的灰色地带。编译器通过，证明就是对的。这是自然语言证明永远无法做到的确定性。

2. AI 不再只是「检索模式」

这些 Erdős 问题没有已知的标准解法。AI 不是在数据库里找到类似题目然后套模板，而是在未知领域自主探索、试错、修正，最终找到人类半个世纪没能找到的路径。

3. 成本低到令人震惊

几百美元解决一道世界级数学难题。放在人类数学家的研究经费尺度上，这几乎等于免费。

4. 改变数学家工作方式

即使 AI 无法完全证明目标定理，它生成的证明尝试也具有研究价值。因为草稿是形式化的，数学家可以直接聚焦于未解决的子目标，无需重新验证整个论证链。AI 不是替代数学家，而是把他们的注意力从繁琐验证中解放出来，投向真正需要人类直觉的缺口。

两条路线的对峙

2026 年 5 月，AI 数学领域同时出现了两条截然不同的路线，而且都取得了突破：

OpenAI 路线：GPT-5.5 Pro 直接输出自然语言证明。菲尔兹奖得主 Gowers 把 Erdős 单位距离猜想扔给它，两小时拿到博士论文级成果，推翻了 80 年猜想。证明极其精妙，但验证它需要人类顶级专家逐行审查。

DeepMind 路线：AlphaProof Nexus 输出 Lean 形式化证明，编译器自动验证。没有主观判断，没有审稿争议，对就是对，错就是错。

两条路线互补，而非互斥。未来最可能的图景是：自然语言探索思路，形式化系统固化验证。 人类数学家提出问题、审查方向、提炼洞见，AI 负责在海量可能性中搜索和严格验证。

开放挑战

AlphaProof Nexus 并非万能：

• Lean 库覆盖范围有限。代数几何、拓扑学等领域的形式化程度远不如数论和组合数学，系统暂时无法触及。
• 复杂证明可能需要数天甚至数周的迭代时间，与人类数学家「灵光一现」的效率相比仍有差距。
• 最困难的开放问题，系统目前仍无法解决——353 个 Erdős 问题只解决了 9 个，成功率约 2.5%。

但趋势已经清晰：随着 Lean 数学库的不断扩展和模型能力的持续提升，这个成功率只会上升。

结语

保罗·埃尔德什生前留下了 1217 道数学难题，悬赏后人求解。他可能从未想过，有一天来领奖的，不是人类。

AlphaProof Nexus 的意义超越了解题本身。它证明了：当 LLM 的创造性直觉与形式化系统的严格约束结合，AI 可以在最抽象、最严谨的人类智力活动中取得确定性进展。

这不是数学的终结，而是数学新纪元的开端。

参考

• 论文：https://arxiv.org/abs/2605.22763
• 来源：谷歌 DeepMind

#AI #数学 #形式化验证 #Lean #DeepMind #Gemini #AlphaProof #Erdős #人工智能 #自动定理证明