Anthropic 宣布完成费马大定理 Lean 形式化,1340 万行代码创纪录
AlexKontorovich · x · 2026-09-05
Anthropic 宣布其内部模型在 prove2.me 平台上完成了费马大定理(FLT)的完整 Lean 形式化证明,这是 Freek Wiedijk「100 大形式化挑战」清单中的最后一项,为这项 20 年的基准画上句号。
关键事实:
- 代码规模超 1340 万行,含 29,500 个中间定理,被称为「迄今最大的 Lean 证明」
- 采用 Darmon–Diamond–Taylor 1995 年对 Wiles–Taylor–Wiles 证明的阐述(经 Langlands–Tunnell 定理与 Ribet 降水平定理),而非现代证明路线
- 仓库开发了 Fontaine 理论及 Mazur 的 Eisenstein 理想工作;证明对指数 n 覆盖有限,但结合已有的正则素数形式化结果,结论完整成立
- 数学家 Kevin Buzzard 在博客中确认:已编译代码并运行 comparator 校验通过;在 96 核机器上编译耗时约为 Lean 数学库 mathlib 的近 20 倍
这被视为 AI 在形式化数学领域的标志性里程碑。
所属事件:Claude 完成 1300 万行 Lean 代码形式化证明费马大定理(23 条相关)→
「研究」频道最新
- VeriPhy:用类型化物理义务对世界模型生成视频做可审计验证 — Wenzhuo Xu · 2026-09-05
- LoRA 作者发博文详解开源模型后训练与 RL 实操 — iamrobotbear · 2026-09-05
- CoT 监控热议下，一视频带你窥探 LLM 内部思维过程 — kastnerkyle · 2026-09-05
- 多智能体辩论可能越辩越错，ICML 论文揭示讨好型失败模式 — ghadfield · 2026-09-05
- 「我们困在巨大的局部最优」：一张旧图引发的 ML 范式讨论 — ZeeshanZiaML · 2026-09-05
- AI 数学证明系统如何工作?Reddit 拆解 Lean 验证流水线设计 — tough-dance · 2026-09-05