Anthropic 用 Claude 在 11 天内形式化证明了费马大定理
来源：anthropic.com — anthropic.com · 697 分 · by jlebar
📋 概述
Anthropic 宣布分享了费马大定理（FLT）的首个完整、可由计算机校验的证明：Claude 在约 11 天内以高度自主的方式用 Lean 证明助手写完全部证明，期间写下 1300 万行 Lean 并证明了 2.95 万个中间定理。社区领军人 Kevin Buzzard 称这是“非凡的自动形式化成就”，不依赖除数学公理外的任何假设。
🔑 核心要点
- Claude 用约 11 天近乎自主完成形式化。
- 写下 1300 万行 Lean 代码。
- 证明了 2.95 万个中间引理与定理。
- 证明仅依赖标准数学公理（propext、Classical.choice、Quot.sound）。
- 由 Kevin Buzzard 等学界专家审阅背书。
💡 金句
机器校验数学证明，就像用计算器核对一次数学计算。
👍 0
👎 0
← 返回 Hacker News 首页