Anthropic 称 Claude 用 11 天完成了费马大定理的首个形式化证明，把已有证明转成 Lean 可逐逻辑步骤检验的形式，代码超过 1300 万行。数十个 Claude 智能体基本自主工作，沿途还产出约 2.9 万个支撑定理的机器可验证证明，覆盖代数、几何、数论与调和分析等此前未被形式化的数学领域。完整证明已在 GitHub 发布。
原文列出 Claude 形式化费马大定理所用代码规模、支撑定理数量与开源入口，读者可据此了解 AI 自动形式化的当前进展。
Respect where respect is due: Anthropic says Claude completed the first fully computer-checked proof of Fermat’s Last Theorem in 11 days.
Andrew Wiles proved the theorem in 1995. Claude’s achievement was turning an existing proof into a form where a computer can check every logical step.
That is much harder than translating text into code. Human mathematicians leave many steps implicit and rely on results scattered across centuries of research. Those dependencies also need precise definitions and proofs.
Working largely autonomously, dozens of Claude agents produced 13 million lines of Lean code and roughly 29,500 supporting theorems, building on existing human work.
Along the way, Claude also produced machine-checkable proofs of roughly 29,500 supporting theorems across algebra, geometry, number theory and harmonic analysis, including mathematics that had never been formalized before.
That could help mathematicians check new research faster, catch hidden gaps, and rigorously evaluate AI-generated proofs. Kudos, Anthropic!
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of the most famous theorems of all time. This was a project experts thought would take many years. It is the largest Lean proof ever written. Fermat’s Last Theorem was first proven in 1995 by Sir Andrew Wiles, more than 350 years after it was conjectured. Our proof, which totals over 13 million lines of code, provides machine verification. More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized. We see this as a major step in the long process of firming up the core of mathematical knowledge, building on work from three centuries of mathematicians and hundreds of contributors to Lean and Mathlib. We are optimistic that AI-assisted verification of mathematical proofs will help reduce the burden of refereeing mathematics in an era where more proofs are being produced than ever before. You can read about the process on our Science Blog: https://t.co/ryYnDEAU6J And see the complete proof on GitHub: https://t.co/wlYMXYnofz在 X 查看被引用的帖子
来源：@kimmonismus · x.com