Claude 11天形式化费马大定理:1300万行Lean代码,29500个定理
机器之心 · wechat · 2026-09-05
Anthropic 宣布 Claude 用 11 天完成费马大定理的完整 Lean 形式化,约 1300 万行代码、30300 个机器可验证定理(29500 个进入最终版),人类只提供少量方向性提示。数学界原本预计这项工程需要数年。
背景：怀尔斯 1995 年的 129 页证明此前从未被完整形式化;2024 年 Kevin Buzzard 发起的社区工程原定以年计。
做法：沿 Darmon–Diamond–Taylor 简化证明路径,数十个 Claude 智能体并行,内部模型(约 Claude Fable 5.1 水平)消耗约 60 亿输出 token。关键脚手架是 Prove2Me 平台:把定理组织成有向无环图管理依赖、拆分陈述与证明文件缩短编译、配自然语言描述供智能体检索——早期多智能体协作失控的 7% 废代码证明没有它走不通。
验证与局限：Lean 仅用三条标准公理通过检查,陈述与 Mathlib 一致;但代码远比 Mathlib 冗长,离简洁可读还很远。
延伸实验：3 个个人版 Claude Max 账号 3 天完成维诺格拉多夫三素数定理形式化,说明普通团队也可参与。更大的意义在于:AI 产出证明速度将远超人类审稿能力,机器形式化验证可能成为数学研究的新基础设施。
所属事件:Claude 11 天完成费马大定理首个形式化证明(52 条相关)→
「漫话AGI」频道最新
- Daniel Lemire：AI 量产论文正在戳穿学术界的「教授庞氏骗局」 — lemire · 2026-10-21
- 学者吐槽:大学封杀爬虫下载论文,终身阅读量不足答辩委员会人数 — generativist · 2026-10-21
- 伯克利获 Schmidt Sciences 资助：用 AI 破解抹香鲸与虎鲸语言 — begusgasper · 2026-10-21
- 3Blue1Brown:即使 LLM 能做清晰讲解,我也会继续做视频 — 3blue1brown · 2026-10-21
- Talos 安全研究员:AI agent 攻击尚是吵闹渗透,蜂群静默红队才是真风险 — matthew_d_green · 2026-10-21
- 3blue1brown 回应争议：AI 产业对数学人才胃口「近乎贪得无厌」 — 3blue1brown · 2026-10-21