Claude 形式化费马大定理：1300 万行 Lean 证明史上最大

asusarla · x · 2026-09-06

Anthropic 宣布 Claude 完成了费马大定理的首次完整形式化证明——将 Andrew Wiles 1995 年的证明转化为 Lean 可机器验证的形式，共超过 1300 万行代码，是迄今最大的 Lean 证明，并顺带形式化了证明所依赖的 29000 多条定理。该项目此前被专家预期需要多年才能完成。

形式化由协同定理证明平台 Prove2Me 辅助，来自 Henry Towsner 的课程项目：Tianyi Peng 的学生 Shuze Chen 参与。平台把论文中的结果拆成小的 Lean 4 任务（mission），任何人都可认领，从而把大规模数学形式化工程化。