Claude 11 天形式化费马大定理，生成 1300 万行 Lean 证明代码
GregCook2011 · x · 2026-09-05
Anthropic 官方宣布，Claude 上个月完成了费马大定理的首次完整形式化证明——即把 Andrew Wiles 1995 年的证明转成 Lean 证明助手可机器验证的形式。专家此前预计这一工作需要多年。
关键事实：
- 最终证明包含超过 1300 万行 Lean 代码，是有史以来最大的 Lean 证明；
- 过程中证明并依赖了约 29,500 个中间定理；
- 数十个 Claude agent 并行工作，把 Wiles 证明中缺失的逻辑细节补全为 Lean 代码，历时 11 天完成（远快于预期的数年）；
- Lean 成功机器验证了最终证明。
意义在于：AI 现在可以自动化"把人类高等数学转成机器可检验证明"这一极其劳动密集的工作，数学形式化的瓶颈可能被大幅打通。
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「研究」频道最新
- 初创公司宣称首次用 AI 设计病毒治疗耐药菌感染患者 — nordicinst · 2026-10-21
- 开源婴儿脑连接工具包:vibe coding 串起皮层-电极-纤维追踪分析 — Dr_Alex_Crimi · 2026-10-21
- 伯克利获 Schmidt Sciences 资助：用 AI 破解抹香鲸与虎鲸语言 — begusgasper · 2026-10-21
- 斯坦福 CS336 第 6 讲:kernel 提速先少跑几趟显存 — stanfordnlp · 2026-10-21
- UIUC 论文：高分不等于会推理，LLM 换个表述就丢失推理规则 — UIUC-CS · 2026-10-21
- 马斯特里赫特研究标注 2122 段真实对话：用户如何向 LLM 求助法律问题 — Amirreza Mohseni · 2026-10-21