Claude 11 天形式化费马大定理

Anthropic 宣布，Claude 已完成首个**端到端、可由计算机完整检查**的费马大定理证明——人类 350 多年未竟的数学名题，被模型连同协作系统耗时约 11 天形式化完成。整项工程约 **1300 万行 Lean 代码、超 3 万个中间定理**,规模超过 Lean 内核数学库 Mathlib 的 5 倍。

完整证明仅依赖 Lean 三个标准公理，最终定理陈述与 Mathlib 中的费马大定理逐字一致，由 Lean 完成逻辑核验。

💡 为什么值得看费马大定理可被计算机检查证明，或提速数学文献形式化。