Claude 11 天自主完成费马大定理 Lean 形式化证明，写了 1300 万行代码

dl_weekly · x · 2026-09-13

Anthropic 宣布获得首个完整、可被计算机验证的费马大定理形式化证明：Claude 在 11 天内基本自主运行，用 Lean 语言写下约 1300 万行代码，证明了 29,500 个中间定理。这项工作由 Anthropic 研究员 Tianyi Peng（其哥伦比亚大学团队研究 AI 形式化）发起，旨在测试 Claude 能否推进 FLT 的形式化，结果远超预期。背景：费马大定理由 Wiles 于 1995 年给出 129 页的人类证明；2024 年起 Kevin Buzzard 在帝国理工学院启动了多年的社区形式化计划。Buzzard 评价称这是非凡的自动形式化成就。文章还讨论了这一工作对研究数学的意义。