Anthropic 用 Claude 在 11 天内完成费马大定理首个机器验证的 Lean 形式化证明
2026.09.05 · 事件 · AI 事件 · 官方发布
Claude 自主编写 1300 万行 Lean 代码，首次实现费马大定理的计算机验证。
Anthropic 研究员 Tianyi Peng 测试 Claude 能否形式化费马大定理，结果 Claude 在 11 天内基本自主完成了首个端到端、计算机检查的证明，编写了 1300 万行 Lean 代码，证明了 29,500 个中间定理。该成果已与 Kevin Buzzard 分享，被认为是自动形式化的非凡成就。
- Claude 11 天完成 FLT 形式化证明
- 编写 1300 万行 Lean 代码
- 证明 29,500 个中间定理
- 首个端到端计算机检查的 FLT 证明
- 成果获 Kevin Buzzard 认可
为什么值得看
AI 自动形式化复杂数学证明，迈向全数学可验证的未来。
适合谁关注
数学家、AI 研究者、形式化验证领域从业者