研究解读 · 2026 年 9 月 7 日
费马大定理早已被证明，Claude 的 11 天改变了什么？
从一个偶数的小例子，理解证明、形式化与机器核查，再看数学家为什么仍有工作要做。
01
发生了什么
已经有了答案，为什么还值得再做一遍？
3² + 4² = 5²，是我们熟悉的一组整数关系。把指数换成大于 2 的整数，就找不到满足 aⁿ + bⁿ = cⁿ 的正整数 a、b、c——这就是费马大定理。它已经有人类证明。这次值得注意的，是把一条已有的复杂证明路线，变成机器可以逐步检查的形式。
Anthropic 9 月 4 日公布，Claude 团队用约 11 天完成 Lean 形式化。使用的是大致相当于 Fable 5.1 的内部研究模型、多个 Agent 和 Prove2Me 协作平台，并有人的高层指导。这是特定研究安排下的结果，不能换算成普通聊天窗口里的一次提问。
- Formalizing Fermat’s Last TheoremAnthropic 研究报告 · 9 月 4 日任务、模型条件、过程与人类工作的说明。
02
看懂形式化
把“显然”展开成可以检查的每一步
先看一个与费马证明无关的小例子：为什么偶数的平方还是偶数？人读到这里往往很快接受。要把理由说完整，需要先说明偶数是什么意思，再展开计算，最后回到定义。
- 先说明条件
n 是偶数：存在整数 k，使 n = 2k。
- 把关系展开
n² = (2k)² = 4k² = 2 × (2k²)
- 回到定义
2k² 仍是整数，所以 n² 也是 2 乘以某个整数。
本站编写的教学推导，帮助理解条件与步骤；不是 Lean 代码，也不是费马大定理的证明。
03
谁来检查
生成论证与接受论证，交给不同环节
Lean 的检查核心按形式规则检查证明。写出证明的可以是人，也可以是 AI；检查不取决于这段话听起来有多自信。复杂证明还依赖许多定义和前面的定理，形式化需要把这些联系明确写出来。
还要确认机器检查的是原本想问的问题。公开仓库的 FinalCheck 文件列出最终陈述和公理检查，README 说明了与 Mathlib 陈述比较的核查流程。本站阅读了固定版本的说明和文件，没有在本机重新编译这份大型证明。
- Theorem Proving in Lean 4Lean 官方教程理解证明助手与检查核心的职责。
- FinalCheck.lean研究仓库 · 固定版本最终陈述与公理检查；本文未重新运行构建。
- README研究团队核查记录核查方式、所需资源与阅读入口。
04
人的工作
机器能够核查，人仍然需要理解
数学家 Kevin Buzzard 在自己的文章中说，他编译了代码并运行 comparator，核查通过。但他的项目还包括把现代数论成果整理进公共数学库，以及制作让人能探索证明的文档。一次大型形式化完成，并不自动完成这些工作。
这也解释了为什么它值得关注：让复杂推理更容易核查，是一种进展；让人看懂为什么成立、哪些中间成果可以复用，又是需要继续做的工作。能检查与容易理解，可以同时追求。
- FLT: Anthropic has beaten me to itKevin Buzzard 本人回应 · 9 月 4 日他的核查经历，以及仍在推进的数学与解释工作。
05
接着看什么
沿着一个问题继续读
想了解故事，可以先读研究报告与 Buzzard 的回应；已有数学背景，再从仓库的 PROOF-PATH 查看各步如何连接。仓库提供了浏览器阅读资料，完整构建则需要较多计算资源。先阅读不必先运行整套证明。
接下来值得研究的是：这类方法能否帮助核查新的数学工作，产物能否更容易阅读和复用，以及形式化过程会暴露哪些原先省略的条件。本文是一次研究解读；这些问题仍需要后续材料，不能由这一个案例直接回答。
- PROOF-PATH.md证明路线 · 固定版本面向有数学背景的读者，连接论证步骤与对应定理。