Claude 用 11 天完成费马大定理首个完整形式化证明，产出约 1300 万行 Lean 代码

Anthropic 宣布 Claude 完成了费马大定理首个端到端、可由计算机完整检查的形式化证明，整个过程用了约 11 天。成果包括约 1300 万行 Lean 代码和超过 3 万个中间定理，规模超过 Lean 核心数学库 Mathlib 的 5 倍。