Claude 11 天写出费马大定理完整 Lean 4 证明并开源：AI 数学的「登月时刻」 · 2026-W36

验证：✔ 已核一手（anthropic.com 研究页 + github.com/anthropics/fermats-last-theorem 仓库，2026-09-07 核）。修正：代码量为「恰好 1300 万行」（官方页原文 13 million lines），每日底稿「逾 1300 万行」表述已修；Lean 4 与 Apache 2.0 在 GitHub 仓库一手确认（发布页未标注）。

时间线

日期	节点
9-5	Anthropic 发布研究：Claude 用 11 天产出费马大定理（FLT）首个端到端机器检验完整证明，代码开源
9-5~6	数学圈与 AI 圈刷屏；Buzzard（Lean 数学界权威）审阅后称「extraordinary autoformalization achievement」
背景	2024 年起 Buzzard 团队的社区项目仍在进行中——Anthropic 抢先撞线

硬参数（双一手核过）

11 天，数十个 Claude Agent「大部分自主」协作（occasional high-level instructions，如 Mazur 定理优先级来自人类 Tianyi）
恰好 1300 万行 Lean 4（4.33.1，Mathlib v4.33.0 pin）——官方称超过 Mathlib 本体 5 倍以上
仓库结构：60,475 个模块、29,511 个定理、1,450 个定义模块；独立内核 nanoda 检查 1,052,234 条声明零错误
仅用 Lean 三条标准公理；comparator 确认定理陈述与 Mathlib 一致（校验约 15 小时、峰值内存 230 GB）
工程栈：Prove2Me 平台（DAG 记录定理依赖）+ Claude Code 多 Agent harness；消耗约 60 亿输出 token；模型为与 Fable 5.1 大致相当的内部研究模型
Apache 2.0 开源（GitHub 仓库一手：anthropics/fermats-last-theorem，844 stars/71 forks，单次提交）
早期失败尝试贡献了最终证明约 7% 的非样板代码行

为什么重要（多角度）

358 年悬案的机器检验完整证明：怀尔斯 1994 年人类证明之后，首个 computer-checked 端到端版本——且主要执行者是 AI；
多 Agent 协作的规模化样本：数十 Agent 并行 + DAG 依赖管理 + 60 亿 token——这是「Agent 完成超长时程任务」迄今最硬的公开案例（直接关联我们 Harness 工程板块）；
对数学研究范式的冲击：Lean 形式化曾是「苦役」，现在 11 天完成过去多年社区工程——Buzzard 们的项目瞬间过时；
能力来自工程而非新模型：用的是与 Fable 5.1 相当的模型——进步主要在 harness 编排，不在基座——「运行时比模型重要」的最新论据。

各方反应

Buzzard：extraordinary autoformalization achievement（其社区项目被超越）
数学 Twitter/知乎：混合惊叹与「形式化 ≠ 理解」的哲学争论
AI 圈：与同期传闻「Claude 已解决纳维-斯托克斯」（？Andrew Curran 单源预测，未证实）叠加，「AI 数学家」叙事升温

来源分级

✔ 一手：https://www.anthropic.com/research/formalizing-fermats-last-theorem
✔ 一手：https://github.com/anthropics/fermats-last-theorem （Lean 4.33.1 / Apache 2.0 / 29,511 定理）
？关联传闻：https://x.com/AndrewCurran_/status/2096062392442724805 （纳维-斯托克斯，未证实勿采信）

写作钩子（我们独有的）

「Claude Code harness 做出的证明」——我们正在学的 Harness 工程板块（上下文压缩、工具执行、权限机制）就是这件事的技术底座：给读者拆解 DAG+并行 Agent+60 亿 token 的编排思路，全网少有人从 harness 视角写；
60 亿 token 换一个定理：算力成本 vs 人类数学家 358 年——「推理成本的单位经济学」绝佳素材；
与 W35「DeepMind 双盲评估」连读：一边是评估 AI 的方法论，一边是 AI 做出数学——AI 与数学的双向奔赴。