Anthropic Claude形式化费马大定理证明

时间：2026年9月4日，Anthropic发布研究文章并开源配套研究产物。 地点：线上，研究由Anthropic研究员及其哥伦比亚大学相关研究团队推进。 人物：Anthropic研究员Tianyi Peng；Imperial College London教授Kevin Buzzard；数学家Andrew Wiles与Richard Taylor是原始证明路线的关键人物。 事件详情：Anthropic称，Claude在大体自主运行11天后，使用Lean证明助手完成了费马大定理（Fermat’s Last Theorem）的端到端计算机检验证明。Claude期间生成约1300万行Lean代码，并证明了约29,500个中间定理。公开仓库显示，最终定理只依赖Lean的三个标准公理，构建目标会检查不存在sorry、额外公理或native_decide；Lean内核和独立Rust内核nanoda均对相关环境进行了检查。 背景：费马大定理断言，当n大于2时，不存在正整数a、b、c满足aⁿ+bⁿ=cⁿ。Andrew Wiles在1990年代完成了纸面证明，但将这套跨越代数、数论、几何等领域的复杂证明完整翻译为机器可检查的Lean代码，一直是长期工程。Imperial College London的Kevin Buzzard团队也在推进另一条“21世纪版本”的形式化路线。 影响：这次成果的核心并不是AI重新发现费马大定理，而是把已有数学证明转化为可复现、可机械检查的形式化证明。它显示，AI可以承担大规模定理翻译、辅助引理构造和证明工程工作，同时把最终正确性判断交给形式化系统；但“机器检查通过”并不替代人类理解中间定理含义，研究仓库也明确将其定位为研究产物。 总结：Claude用11天完成费马大定理首个端到端计算机检验证明，并将证明开源。该事件更像是AI加速数学形式化与验证的工程里程碑，而不是AI独立攻克一个尚未解决的数学猜想。 参考来源： 1. Anthropic官方研究文章：https://www.anthropic.com/research/formalizing-fermats-last-theorem 2. Anthropic开源Lean证明仓库：https://github.com/anthropics/fermats-last-theorem 3. Lean官方费马大定理形式化项目介绍：https://lean-lang.org/use-cases/flt/ 4. Imperial College London FLT项目：https://github.com/ImperialCollegeLondon/FLT 5. New Scientist相关报道：https://www.newscientist.com/article/2533518-mathematicians-put-ai-to-work-on-fermats-last-theorem/ 6. All The News相关报道：https://allthe.news/zh/articles/mathematicians-advance-fermat-last-theorem-formalization-with-ai