Claude 用 11 天把费马大定理做成机器可校验的证明

2026 年 9 月 4 日，Anthropic 在官网发布研究报告《Formalizing Fermat's Last Theorem》。报告说：他们用 Claude 在 11 天内，把怀尔斯 1994 年的费马大定理证明，重写为 Lean 形式化证明，最终由 Lean 编译器逐行跑通。

这件事的历史分量要放在 358 年的尺度上看。1637 年费马在书页边上留下那句著名的"空白太小写不下"，之后几代数学家接力，直到怀尔斯在 1994 年给出一个 150 页、依赖现代数论最前沿工具的证明——那个证明全世界只有几十个人能完整读懂。2026 年秋天，Claude 做的不是"重新证明"，而是把那 150 页人类证明翻译成 Lean 代码，让编译器说出一句 Q.E.D.。

意义不在"AI 比怀尔斯聪明"，而在"这道题从此不再只属于那几十个专家"。任何一个 Lean 用户都可以打开文件，从头读到尾，看到每一步严格合法的证明。来源：Anthropic 官方 2026-09-04（anthropic.com/research/formalizing-fermats-last-theorem）。

关联阅读：形式化验证 Lean 是什么，为什么它成了 AI 数学的"裁判"。