AI完成费马大定理形式化证明：Claude用11天干完了数学家几年的活

2025年8月18日，Anthropic宣布：Claude完成了人类历史上第一个端到端、计算机可验证的费马大定理形式化证明。整个过程仅用了11天，写下了1300万行Lean代码，证明了29,500个中间定理。

这不是在开玩笑。

一、费马大定理是什么？

1637年前后，法国数学家皮埃尔·德·费马（Pierre de Fermat）在阅读丢番图（Diophantus）的《算术》一书时，在书页边缘潦草地写下了一个命题：

我发现了一个绝妙的证明，但这里空白太小写不下。

这个命题后来被称为费马大定理（Fermat's Last Theorem，简称FLT）：

当整数 n > 2 时，不存在正整数 a、b、c 能满足 aⁿ + bⁿ = cⁿ。

就这么一句看似简单的话，人类用了358年才彻底证明它。

二、为什么证明这么难？

费马大定理是数学史上最著名的"幽灵"。

1908年，德国悬赏10万金马克（相当于今天的100-200万美元），一年内就收到了621份错误的证明。此后一百多年，一代代顶尖数学家前赴后继，无功而返。

1993年，英国数学家安德鲁·怀尔斯（Andrew Wiles）终于宣布证明了FLT——但在两个月的严格审查中，一位审稿人发现了一个关键性漏洞。怀尔斯用了一年时间修补，最终在1995年发表了完整证明，整篇论文长达129页。

怀尔斯的证明用到了现代数学最深的工具：椭圆曲线、模形式、伽罗瓦表示、拓扑学……远远超出了1637年费马可能掌握的任何知识。因此数学界现在普遍认为，费马当年那个"绝妙的证明"很可能是错的。

三、形式化证明：让计算机来验证数学

什么是形式化证明？

人类写的数学证明充满了"显而易见"、"同理可得"、"由对称性可知"这样的省略。人类审稿人能理解，但计算机无法验证。

形式化（Formalization） 就是把数学证明用一种严格的编程语言写出来，让计算机逐行检查逻辑是否成立。这种工具叫证明助手（Proof Assistant），最著名的就是Lean。

Lean由微软研究院开发，它的原理是：每一个数学陈述都要有严格的逻辑推导，每一个中间步骤都不能省略。如果证明中任何一步有漏洞，Lean会直接报错。

形式化为什么难？

传统数学证明依赖人类读者的专业经验省略大量步骤，而形式化后的证明必须展示每一个逻辑步骤，且只能引用已经形式化过的数学库。怀尔斯1995年的证明，数学界预期其形式化需要数年时间。2024年，帝国理工学院的Kevin Buzzard才刚启动这个项目。Claude的结果：11天完成。

四、Claude是如何做到的？

Prove2Me平台

Anthropic的研究者Tianyi Peng设计了一个名为Prove2Me的开放协作平台，专门用于数学形式化。它的核心是一个有向无环图（DAG），记录了所有定理陈述和它们之间的依赖关系。

关键特性：

• 并行化：多个AI Agent可以同时工作，各自证明不同的子定理
• 依赖管理：每个Agent知道哪些定理已经被证明，从而决定下一步该证明什么
• 搜索复用：每个定理陈述都有自然语言描述，方便搜索和复用
• 加速编译：将定理陈述和证明分开到不同文件，减少编译开销

多Agent协作架构

Claude团队使用了Claude Code多Agent架构，类似于软件开发中的流水线：多个Agent并行工作，每个负责证明某个子定理，证明完成后其结论被其他Agent使用，通过DAG管理依赖关系避免冲突。

初期尝试遇到了困难：Agent们很快就失去了对项目全局状态的追踪，协作效率低下。失败的努力贡献了最终证明中约7%的非模板代码。后来切换到Prove2Me平台后，效率大幅提升。

用了多少算力？

整个项目消耗了约60亿个输出Token，使用了一个与Claude Opus 4.1能力相当的通用研究模型。这个证明是Mathlib（Lean最大的数学库）代码量的5倍以上。

五、验证工作：三层保险

第一层：Lean内核验证

整个仓库的60,475个模块全部编译，Lean内核逐行检查每一条声明。只依赖了Lean的三条标准公理（propext、Classical.choice、Quot.sound），没有使用任何"Sorry"或额外公理。

第二层：comparator独立验证

使用Lean官方团队开发的comparator工具，将证明与Mathlib中已有的FLT陈述进行比对。验证结果确认所证明的定理陈述与Mathlib中的FLT标准陈述完全一致。

第三层：nanoda第二内核

nanoda是一个用Rust独立编写的Lean内核。它对导出的声明进行了完整验证：1,052,234条声明全部通过验证。

三套独立工具，全部通过。

六、项目设计哲学

1. 极简公理基础

整个证明只依赖Lean的三条标准公理，没有引入任何额外假设，不使用sorry作为证明占位符。

2. DAG驱动的任务分配

Prove2Me的DAG设计是核心创新，将证明分解为可独立完成的单元任务，解决了AI Agent的"记忆退化"问题。

3. 可视化与可读性

项目中包含完整的HTML文档站点（约390MB），可在浏览器中离线浏览，逐步展示证明路径，每个定理有独立页面展示其Lean陈述、引用关系和可展开的依赖图。

4. 透明与可复现

所有源代码开源（Apache 2.0许可），构建脚本公开，验证过程可独立复现。

5. 渐进式构建策略

采用分而治之的策略：将复杂证明分解为数千个子定理，逐步证明，逐步集成。这种策略使AI Agent能够有效工作，也便于在失败时精确定位问题。

七、里程碑意义

数学验证的范式转变

过去验证一个重要数学证明可能需要数年时间。AI形式化证明的出现，意味着这个过程可以大幅缩短。

Kevin Buzzard审阅后说：

如果FLT的自动形式化现在是可能的，那么我们已经在自动形式化现代数学文献的道路上迈出了一大步。

对AI生成数学的信任

随着LLM越来越多地参与数学研究，形式化证明成为验证AI数学结论的关键工具。

全民AI数学家的时代来临？

Anthropic用三个个人Claude Max订阅账号，通过Prove2Me协作，在3天内完成了Vinogradov三素数定理的形式化。这意味着普通消费者级别的AI订阅也能完成重大数学定理的形式化。

八、技术细节：项目结构一览

fermats-last-theorem/
├── Theorems/          # 所有定理陈述声明
├── P2M/Sol/          # Prove2Me格式的证明
├── Definitions/       # 必要的数学定义
├── verification/
│   ├── comparator/   # 与Mathlib对比验证
│   └── nanoda/       # 独立Rust内核验证
├── html/             # 可离线浏览的证明站点
└── tools/docs-site/  # 文档生成工具

构建要求：Linux或macOS、elan工具链、约67GB磁盘空间、约153GB内存峰值。

九、核心结论归纳

1. AI形式化数学证明已经完全可行：费马大定理这个被预期需要数年人力工作的项目，AI在11天内独立完成

2. 多Agent协作是规模化形式化的关键：Prove2Me的DAG架构解决了并行化问题，使多个Agent能够高效协作

3. Lean作为"数学操作系统"的成熟度：Mathlib积累了数千条已形式化的定理，为更复杂的证明提供了基础设施

4. 三重验证体系确保可靠性：Lean内核 + comparator + nanoda独立内核，三套独立工具交叉验证

5. AI正在改变数学研究的信任机制：未来，形式化证明可能成为数学论文的标准附件

6. 开源与透明是科学进步的基础：整个证明过程、开源代码、验证工具全部公开，任何人都可以复现和检查

十、给普通人的启示

费马大定理的形式化证明不仅仅是一个技术成就，它预示着几个重要趋势：

• 数学知识的可靠性将大幅提升：形式化证明可以消除人类审稿中不可避免的疏忽和偏见
• AI将成为数学家的"副驾驶"：帮助验证、发现和构建更复杂的证明
• 科学知识的生产方式正在改变：从个人英雄主义到协作网络，从纸质论文到可执行证明

358年前，费马在书页边缘留下了一个"空白太小写不下"的证明。358年后，Claude用1300万行代码把这个证明完整地写了出来，并且让计算机逐行验证了它的正确性。

这不是终点，而是开始。