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 11 天完成费马大定理首个形式化证明(52 条相关)→
「研究」频道最新
- CMU 与 Meta 开源 TrackEverything：追踪长视频全部 3D 点 — AdamWHarley · 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