Anthropic 宣布其 AI 模型 Claude 在 11 天内基本自主完成了费马大定理的 Lean 形式化证明，这是首个完整的计算机验证证明。该证明包含 1300 万行 Lean 代码，证明了 30300 个中间定理，规模超过 Mathlib 五倍。
Anthropic 用 Claude 在 11 天内完成费马大定理首个机器验证的 Lean 形式化证明