Claude 11天完成费马大定理形式化：1300万行代码60亿Token
新智元 · wechat · 2026-09-05
Anthropic 宣布 Claude 仅用 11 天、以「基本自主工作」方式完成了费马大定理的首个端到端 Lean 机器验证证明，人类数学界原本预计这项形式化工程要以年为单位。核心数据：生成约 1300 万行代码、产出 30300 条可验证定理（29500 条被采用）、消耗约 60 亿 Token，体量超过 Mathlib 定理库的 5 倍，是迄今最大的 Lean 证明。费马大定理 1637 年提出、1995 年才由怀尔斯用 129 页论文证明，人类验证这类证明常需数月乃至数年。
过程要点：
- 形式化必须从公理逐层搭建，Claude 顺带证明了约 29000 条中间定理，覆盖代数、几何、数论、调和分析等此前未被形式化的分支，最终 Lean 编译全部通过、仅依赖三条基础公理。
- 早期几十个智能体协作曾彻底乱套，失败尝试代码仅占最终 7%；关键救场的是哥伦比亚大学助理教授、Anthropic 研究员彭天翼（清华姚班出身）团队的 Prove2Me 平台：用定理 DAG 任务树给智能体分工导航、陈述与证明分离加快编译、自然语言索引方便检索复用。
- 作为「秀肌肉」的附加实验，3 个普通账号用 3 天就在 Prove2Me 上形式化了数论中的维诺格拉多夫三素数定理。
数学界评价极高：帝国理工 Kevin Buzzard（原计划花数年搞费马形式化）称这是现代数学文献自动形式化的一大步。Anthropic 的判断是 AI 不会取代数学家，但会把「附带形式化验证代码」变成论文标配，终结数学史上「99% 确定」式的验证悲剧。
所属事件: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