Formalizing Fermat's Last Theorem

Anthropic 说 Claude 用 11 天基本自主生成 Lean 中完整、可机检的费马大定理证明，写下约 1,300 万行 Lean 和 29,500 个中间定理。贡献不是替代 1995 年的数学证明，而是把跨代数、几何、调和分析和数论的长证明转成可由 proof assistant 检查的结构化工件；这也暴露自动形式化的真正成本在库接口、类型化中间引理和错误恢复，而非只在最终 theorem。