姚班校友主导，Claude攻克费马大定理首个完整形式化证明
2026.09.05 · 事件 · AI 事件 · 官方披露
Anthropic 用 Claude 在 11 天内完成费马大定理的完整形式化证明，代码量超 1300 万行。
Anthropic 宣布，Claude 在 11 天内完成了费马大定理的首个端到端形式化证明，生成约 1300 万行 Lean 代码、超过 3 万个中间定理，规模超过 Lean 核心数学库 Mathlib 的 5 倍。项目由清华姚班校友、哥伦比亚大学助理教授 Tianyi Peng 主导，使用多 Agent 协作和 Prove2Me 平台，最终证明经 Lean 验证。
- Claude 11 天完成费马大定理形式化证明
- 生成约 1300 万行 Lean 代码，超 3 万中间定理
- 代码量超过 Mathlib 核心库 5 倍
- 多 Agent 协作，使用 Prove2Me 平台
- 消耗约 60 亿输出 Token
为什么值得看
AI 首次完成超大规模数学形式化，效率远超人类多年计划。
适合谁关注
关注 AI 数学能力、形式化验证和前沿模型应用的读者。