Anthropic 内部模型 11 天用 Lean 形式化费马大定理,超 1340 万行证明
sammcallister · x · 2026-09-05
数学家 Kevin Buzzard（Xena 项目）撰文确认：Anthropic 一个内部模型借助 prove2.me 平台，在 Lean 中完成了费马大定理（FLT）的完整形式化证明，仅用 11 天，也终结了 Freek Wiedijk 著名的「100 个形式化挑战」清单——最后一个被攻克的定理。
- 证明路线：采用 1995 年 Darmon–Diamond–Taylor 对 Wiles–Taylor–Wiles 论证的阐述，经 Langlands–Tunnell 定理与 Ribet 降级定理；代码库自行发展了 Fontaine 理论与 Mazur 的 Eisenstein 理想工作。
- 规模与验证：证明超 1340 万行 Lean 代码，在 96 核机器上编译耗时约为 Lean 数学库 mathlib 的 20 倍；Buzzard 编译并跑 comparator 验证通过。因未完整形式化 Mazur 关于 Frey 曲线的结论，此证明仅覆盖部分指数情形，但结合已有的正则素数形式化，结论完整成立。
- 意义：展示了 AI 形式化（autoformalization）产物已足够健壮、可被复用和叠加，涵盖代数、调和分析、几何与数论的多层形式化。
所属事件:Claude 完成 1300 万行 Lean 代码形式化证明费马大定理(20 条相关)→
「研究」频道最新
- MultiMDM:让掩码扩散语言模型「先打草稿」实现少步生成 — QuanquanGu · 2026-09-05
- Google DeepMind 推出免费在线书《How To Scale Your Model》讲透 TPU 上 LLM 扩展 — goyal__pramod · 2026-09-05
- 开发者优化 MoE 内核:BF16 提速 1.2 倍,MXFP8 提速 1.6 倍 — retr0jirachi · 2026-09-05
- 数学家 Kevin Buzzard 独立验证 Anthropic 的 FLT Lean 证明:确实成立 — AlexKontorovich · 2026-09-05
- Prime Intellect 用 NIXL 把万亿参数 RL 权重同步从 86 秒压到 4 秒 — samsja19 · 2026-09-05
- Karpathy「先过拟合再正则化」原则在大规模后训练时代依然成立 — rdesh26 · 2026-09-05