AI 刚刚证明了费马大定理？别急，真相可能和你想的不一样。

01

一个吓人的标题

昨天我朋友圈被刷屏了，标题一个比一个吓人：「AI 证明了数学史上最难定理」「Anthropic 击败人类数学家」。说真的，第一眼看过去我也心头一紧，费马大定理啊，这玩意儿困扰了数学界 358 年，直到 1995 年才被安德鲁·怀尔斯用 100 多页的论文搞定。

但冷静下来读完原始材料，我发现事情没那么简单。准确说，这是 Lean 4 形式化验证 框架下的一个里程碑，不是 AI「独立思考」出来的证明。

这更像是一场精密的工程协作，而非 AI 的顿悟时刻。

02

技术上来说，到底发生了什么

简单讲就是，Anthropic 的 AI 系统协助数学家 Kevin Buzzard 的 Xenaproject 团队，把费马大定理（FLT）的一个关键部分——也就是 模形式与椭圆曲线的关联——用 Lean 4 代码形式化了一遍。Lean 4 是微软研究院开发的交互式定理证明器，你可以把它理解成一个极度严谨的代码编辑器，它会检查你的每一步数学推理是否在逻辑上无懈可击。

这里有个细节很有意思。费马大定理的原始证明极其复杂，涉及到 谷山-志村猜想（现在叫模性定理）的大量前置工作。要把这整个证明「翻译」成机器可验证的代码，工作量巨大到令人绝望。Kevin Buzzard 的团队干了好几年，这次是 AI 帮他们大幅加速了这个过程。

具体是怎么加速的？我猜大概是这样：AI 负责生成大量的中间证明步骤和引理，人类数学家负责审查和修正，然后 Lean 4 作为终极裁判来验证。整个流程下来，AI 的角色更像一个超级勤奋的研究助理，而不是那个拍板的首席科学家。

03

同期谁还在干这种事

这不是一个孤立事件。过去两年，AI + 形式化数学验证这个赛道突然火了。

1DeepMind 的 AlphaProof 在 2024 年 IMO 竞赛上拿了银牌级别的成绩，用的就是强化学习 + Lean 的路线。

2OpenAI 虽然没单独搞形式化验证，但 GPT-4 和后续模型在数学推理上的进步有目共睹，Sam Altman 在 X 上多次暗示他们在数学 AI 方向有大动作。

3Meta 的 FAIR 实验室也开源了一些数学推理数据集和基准测试工具。

4更不用说 Lean 社区本身，那帮人一直在用传统程序分析的方法推进形式化验证，比如 Xena 项目本身就是在 Kevin Buzzard 主导下跑了好几年。

整个行业的趋势很明显：大家不再满足于 AI 能算对一道题，而是要让它参与到「证明」这个更高级的认知活动中去。 这两者差别巨大。算对题是 pattern matching，证明是需要构建逻辑链条的。

04

对行业意味着什么

先说结论：这件事对 AI 公司来说，是一个巨大的 PR 胜利，但对数学界来说，意义更深远。

对 Anthropic 而言，这几乎是一个完美的技术营销案例。Claude 系列模型一直强调安全性和可靠性，现在他们能说：「你看，我们的 AI 帮忙证明了人类历史上最著名的数学定理之一。」这比跑分刷榜有说服力多了。但我要泼一盆冷水——这次的核心技术突破可能不在 AI 模型本身，而在 人机协作流程的优化。换句话说，换一个足够聪明的模型（比如 GPT-4o 或 Gemini 1.5 Pro），在同样的团队和流程下，可能也能做到类似的事。

那真正的护城河在哪？我觉得是 数据飞轮。每一次这样的协作，都会产生大量的高质量形式化证明数据。这些数据反哺给模型训练，模型又能在下一次任务中表现更好。Anthropic 如果能把这条路跑通，后面的竞争对手想追就很费劲了。

05

普通人/从业者为什么要关心

你可能觉得，我又不是数学家，费马大定理跟我有什么关系？关系大了。

想象一个场景：你是一个航空航天工程师，需要验证某个关键结构设计的安全性。传统方法是跑大量仿真，然后靠人类专家审查。但如果未来 AI + 形式化验证的工具成熟了，你可以把设计参数丢给 AI，让它自动生成一个 机器可验证的安全性证明。这个证明不是「大概率没问题」，而是「在公理体系内绝对没问题」。这在金融风控、芯片设计、医疗设备认证这些领域，价值无可估量。

当然，现阶段还远没到那一步。形式化验证的门槛依然很高，Lean 4 的学习曲线陡峭得像悬崖。但 Anthropic 这次的成果至少证明了一件事：AI 可以显著降低这个门槛。 以前一个博士生可能要花两年才能形式化一个中等复杂度的定理，现在有了 AI 辅助，可能几个月就能搞定。

06

跟竞品比，Anthropic 强在哪

拿 DeepMind 的 AlphaProof 对比一下。AlphaProof 用的是强化学习，本质上是让 AI 自己「摸索」出证明路径，人类参与度更低，但目前只能处理竞赛级别的问题，离数学前沿还差得远。Anthropic 这次的方法更像是 人类专家主导 + AI 辅助，虽然「自主性」不如 AlphaProof，但能处理的问题复杂度高了好几个数量级。

现阶段，「人在回路」的协作模式可能比「纯自主 AI」更适合啃硬骨头。

还有一点值得说：Anthropic 选择跟学术界合作（Xenaproject 是帝国理工的项目），而不是自己闭门造车，这个策略我觉得很聪明。形式化数学验证这东西，脱离了数学家的深度参与，AI 再强也玩不转。这跟 AI 写代码不一样——代码可以跑测试，数学证明错了就是错了，没有「差不多能用」这一说。

07

一句话判断

Anthropic 这次是真有东西，但别被标题党带偏了。AI 还没有「证明」费马大定理，它是在人类指导下参与了一个宏大的形式化工程。真正的意义在于：人机协作做数学前沿研究这条路，被验证走得通了。 现阶段值得关注，但离「AI 数学家」还有十万八千里。

本文基于 developer 公开报道编译解读，查看原文