Anthropic: Claude formalizes Fermat's Last Theorem proof in Lean over 11 days
Anthropic announced that its AI model Claude worked largely autonomously over 11 days to produce the first complete computer-checked proof of Fermat's Last Theorem, formalized in the Lean programming language. The effort involved about 13 million lines of Lean code and over 30,000 intermediate theorems, with the final proof using roughly 29,500 of them. The project, which did not introduce a new proof but translated the existing human-readable proof into machine-checkable form, is more than five times the size of Lean's core math library Mathlib.
Coverage timeline
Anthropic Research
Sep 4, 2026ScienceFormalizing Fermat's Last Theorem
Techmeme
Anthropic : Anthropic says Claude worked “largely autonomously” over 11 days to formalize the proof of Fermat's Last Theorem in the Lean programming language — We are sharing the first complete computer-checked proof of Fermat's Last Theorem. Claude worked largely autonomously over 11 days …
量子位量子位
< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400"> 2026-09-05 09:17:56 来源：量子位 最后靠Harness救回来 ## 梦瑶 发自 凹非寺 ## 量子位 | 公众号 QbitAI 人类和费马大定理纠缠了三个半世纪，Claude这次只用了11天！？ 刚刚，Anthropic宣布，Claude完成了首个端到端、可由计算机完整检查的**费马大定理证明**。 约1300万行Lean代码、超过3万个中间定理、最终证明使用其中约29500个。 整个工程规模，已经超过Lean核心数学库Mathlib的**5倍**。 这次Claude没有发现一个全新的费马大定理证明。 它完成的是另一件同样工程量《惊人》的工作： 把人类数学家能够读懂的证明，彻底翻译成计算机能够一行一行检查、没有任何「这里显然」的形式化证明。 而这件事，数学界原本是按多年工程来准备的？？？？ ## 350多年数学史，被Claude塞进1300万行Lean 先快速说一下费马大定理到底是什么。 其指的是，对于任意整数n>2，都不存在正整数a、b、c，使：**aⁿ+bⁿ=cⁿ**。 这个命题看起来极其简单，难度却高得离谱！！ 从17世纪费马留下这个命题开始，欧拉、勒让德、库默尔等一代代数学家不断往前推进，始终没能拿下完整证明。 直到1993年，英国数学家Andrew Wiles第一次公开宣布证明费马大定理。 随后审查发现其中存在关键缺口。 Wiles又花了大约一年时间和Richard Taylor一起修补，最终在1994年完成证明，到这里，困扰数学界350多年的命题才终于被攻克。。。 But！数学界随后又给自己挖了一个更工程化的坑—— **能不能让计算机，也百分之百确认这份证明成立捏？** 这就是所谓的「形式化」。 简单理解，普通数学论文是写给数学家看的，人脑看到很多步骤，可以直接说：嗯，这里显然成立～ 但Lean这种专门检查数学证明的程序系统证明助手，可不吃这一套。。。 我们可以把**Lean**理解成数学世界里的「超级严格编译器」—— 数学家或者AI负责把定理、定义和证明一步一步写成Lean能够理解的形式；Lean则负责检查
机器之心机器之心
费马大定理，终于有了一份能由计算机从头检查到尾的完整证明。 就在刚刚，Anthropic 声称，Claude 在 11 天内完成整个工程，写下约 1300 万行 Lean 代码，过程中人类只提供了少量高层指导。 完整的证明请参见 GitHub：https://github.com/anthropics/fermats-last-theorem 这次 Claude 没有提出新的证明路线，它所做的是把已有证明转写成机器能够逐步核验的形式，让每一个逻辑环节都接受计算机检查。 对于费马大定理这样的世纪难题，此前数学界普遍预计，完整的形式化工程需要数年时间。 为什么费马大定理还要再「证明」一次？ 1637 年前后，法国数学家皮埃尔・德・费马在《算术》一书的页边写下一个判断：当整数 n 大于 2 时，不存在满足 aⁿ+bⁿ=cⁿ的正整数 a、b、c。 他还留下一句：自己已经找到了一个「绝妙的证明」，只是页边太窄，写不下。 此后的 350 多年里，一代代数学家不断尝试。1993 年，安德鲁・怀尔斯在三场讲座中公布证明。两个月后，审稿人发现其中存在关键缺口。怀尔斯与理查德・泰勒又花费近一年完成修补，最终于 1995 年发表长达 129 页的完整证明。 费马大定理从此有了公认答案，但验证大型数学证明仍高度依赖人类。 数学论文通常会省略显而易见的步骤，也会直接调用前人已经建立的结论。面对一条跨越多个领域的复杂证明，审稿人需要逐层追踪它依赖的定义、定理与推导。整个过程往往持续数月，甚至数年。 形式化证明给出了另一种检查方式。 研究者先把自然语言中的数学推理写成 Lean 等证明助手能够理解的代码，Lean 再依据明确的公理和规则，逐步检查逻辑是否成立。人类可以略去的步骤，在这里都要补全。 2005 年前后，荷兰计算机科学家 Jan Bergstra 提出将怀尔斯的证明形式化。2024 年，帝国理工学院数学家 Kevin Buzzard 又发起了一项长期社区工程，尝试用 Lean 完成这件事。仅项目第一阶段的技术蓝图就有 86 页，原定周期以年计算。 11 天，3 万多个定理，1300 万行代码 Anthropic 研究员 Tianyi Peng 最初只是想测试，Claude 能否推动这项工程继续向前。结果很快超出预期。 Claude 沿用了 Henri Darmon、Fred Diamo
