Claude 11 天完成费马大定理形式化，1300 万行 Lean 代码超 Mathlib 5 倍
量子位 · wechat · 2026-09-05
Anthropic 宣布 Claude 完成首个端到端、可由计算机完整检查的费马大定理形式化证明：约 1300 万行 Lean 代码、超过 3 万个中间定理（最终使用约 29500 个），代码量超过 Lean 核心数学库 Mathlib 的 5 倍。这不是新证明，而是把 Wiles 1994 年的人类证明完整翻译成 Lean 可逐行检查的形式化版本——原本数学界按多年工程准备的项目，Claude 只用了 11 天。
关键细节
- 主导者是 Anthropic 研究员、哥大助理教授 Tianyi Peng（清华姚班毕业、MIT 博士），最初只是测试能推进多远，结果一路做到终点。
- 过程采用多 Agent 并行：分别负责数学定义、中间引理、高层定理推进与最终拼装，消耗约 60 亿输出 Token，内部模型能力约相当于 Claude Fable 5.1。
- 早期多 Agent 协作失控，失败尝试只占成品代码约 7%；换用专为形式化搭建的 Prove2Me 平台后才扭转——该平台把证明拆成定理节点的 DAG，管理依赖、加速 Lean 编译、保留自然语言描述供检索复用。
- 人类数学指导极少，仅偶尔给出高层优先级提示；最终证明仅依赖 Lean 三个标准公理，并通过比对程序确认与 Mathlib 中定理陈述完全一致，由 Lean 而非模型自己担任裁判。
- 审阅人、帝国理工 Kevin Buzzard 评价为「非凡的自动形式化成果」，意味着大规模数学文献形式化首次具备提速条件。
One more thing：同期 OpenAI 开始向 Pro/Business/Enterprise 用户推送 GPT-6 Astra，强化长链路 Agent、软件工程、计算机操作与科学工作等能力。
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「编程与Agent」频道最新
- LukeW 总结智能体软件五大 UI 难题:多智能体监控与协作设计 — LukeW · 2026-10-21
- 用 Claude Code 经 ADB 清理安卓电视:删 11 个应用、可用内存涨 90% — edwinarbus · 2026-10-21
- 小米电视被广告件拖到卡顿,开发者用 Claude 一键救回流畅 — edwinarbus · 2026-10-21
- 开源新模型 Ornith-1.5-122B 发布:SWE-bench 84.5%,单卡 DGX 可跑 — _akhaliq · 2026-10-21
- 用 Claude Code 给智能电视「瘦身」去广告成新 trend — edwinarbus · 2026-10-21
- Claude Code 隐藏设置 crossSessionInbound 被指是蜂群 agent 的关键原语 — kieranklaassen · 2026-10-21