AI首次形式化证明费马大定理（2026‑09‑04，Anthropic）

重点澄清：AI没有“重新发现”费马大定理，而是把怀尔斯1995年的人类证明，转译为机器可逐行校验的形式化代码，完成端到端计算机核验。

事件概况

- 发起者：Anthropic研究员彭天翼（Tianyi Peng，清华姚班校友），基于Prove2Me多智能体协作平台，调度数十个Claude智能体协同工作。

- 工具：Lean 4（交互定理证明器，不接受“显然”，每一步逻辑必须严格写清、内核自动校验）。

- 耗时：11天基本自主运行，人类只做少量任务优先级指引。

- 规模数据：

- 生成约 1300万行Lean代码

- 产出30300条中间定理，最终证明链用到29511条

- 消耗约60亿输出token

- 验证：帝国理工学院数学家Kevin Buzzard亲自编译运行代码，确认全部通过机器校验，无未证明假设，完全从数学公理出发推导出费马大定理结论。

背景回顾

1. 费马大定理：整数 n>2，方程 x^n+y^n=z^n 不存在正整数解。1637年费马提出猜想，留下“页边太窄写不下证明”的名言 。

2. 人类原始证明：1995年安德鲁·怀尔斯（Andrew Wiles）完成，129页论文，融合椭圆曲线、模形式、伽罗瓦表示等深奥代数数论；人类审稿就耗费数月，论文中大量“显然可得”的省略推理，不适合机器直接阅读。

3. 形式化难题：把怀尔斯的证明翻译成Lean，学界预估人类团队要5‑10年才能做完；此前社区只完成部分局部引理的形式化，没有完整端到端版本 。

什么是“形式化证明”？

- 普通数学论文：写给人读，允许省略熟悉的推导，写“易证、显然”。

- 形式化证明：把每一条定义、每一步推理全部写成机器可理解代码；Lean内核逐行检查逻辑，只要代码编译通过，就代表证明逻辑绝对成立，不存在人为疏漏。

- 本次的本质：AI把人类已经得到的证明，完成完整机器翻译与核验，不是AI自己想出一套全新证明思路。

意义与业界评价

1. 数学形式化里程碑：证明AI多智能体可以处理现代数学里极复杂的长链条证明，未来可以用来核验大量人类数学论文，减少人工审稿错误 。

2. 数学界观点：

“如果费马大定理可以被AI完整形式化，那么几乎所有现代数学都可以做到。”——Daniel Litt（多伦多大学数论学家）

3. 局限：AI目前还不能独立提出全新数学猜想、发现全新证明思路，擅长把已有人类证明转成机器可验证的严谨版本。

公开资源

- 官方博客：Anthropic《Formalizing Fermat’s Last Theorem》

- 开源代码仓库：github.com/anthropics/fermats‑last‑theorem