post cover

AI 热点快报：Claude 用 Lean 端到端证明费马大定理，首个完整机器可验证证明诞生（2026-09-06）

事件与背景

北京时间 9 月 5 日凌晨（美东 9 月 4 日），Anthropic 发布研究公告：其 Claude 模型在「基本自主」状态下用 11 天，在 Lean 证明助手中写出了费马大定理（FLT）的首个端到端、经计算机完整校验的证明。费马大定理声称：对任意 n＞2，aⁿ＋bⁿ＝cⁿ 不存在正整数解。它由 Andrew Wiles 在 1995 年给出 129 页的人类证明，此后三十年无人完成机器形式化；2024 年起 Kevin Buzzard 在帝国理工学院发起的社区形式化项目（配套 86 页 blueprint）原本预计要耗时数年——这次 Anthropic 抢先撞线，HN 讨论中有人直言「Buzzard 的团队被截胡了」。

公告中的关键事实（均出自 Anthropic 官方页面）：

  • 规模空前：证明约含 1300 万行 Lean 代码，超过 Mathlib（Lean 社区核心数学库）体量的 5 倍；过程中共证明 3.03 万个定理，最终证明用到其中 2.95 万个。
  • 成本量级：消耗约 60 亿输出 token，运行在「大致对标 Claude Fable 5.1 的内部通用研究模型」上；数十个 Claude agent 通过 Claude Code 多 agent 框架并行协作，人类数学输入仅限研究者 Tianyi Peng 偶尔下发的高层指令（如「Jacobian 作为 scheme 是优先项」「把 Mazur 定理尽快推完」）。
  • 正确性背书：Lean 内核逐行机械检查，只依赖 Lean 的三个标准公理；comparator 工具确认定理陈述与 Mathlib 自带的 FLT 陈述一致；Buzzard 亲自审阅后评价这是「非凡的自动形式化成就……除数学公理外无任何假设」。
  • 过程并非一帆风顺：Anthropic 坦承早期多次尝试失败——agent 们很快丢失项目状态、停止有效协作，失败尝试贡献了最终证明约 7% 的非样板代码行。转折点是改用 Peng 与哥伦比亚大学合作者设计的开源平台 Prove2Me：用有向无环图维护定理依赖、把定理陈述与证明拆成不同文件、并为每条定理维护自然语言描述以便检索复用，从而缓解了长程任务中的记忆衰减。
  • 溢出实验：Anthropic 用三份个人 Claude Max 订阅、完全经由 Prove2Me 协作，仅 3 天就形式化完成了 Vinogradov 三素数定理——「消费级订阅也能协作形式化重大定理」。

来源：

为什么现在重要

  1. 「AI 数学」的验证侧首次跑赢发现侧。 与近期 AI 在黎曼假设上的工作（产出的是新数学、未经机器验证）不同，Anthropic 明确指出这次的新颖点在 verification——用计算机像验算一样核验一个庞大的人类证明。影响判断：当「AI 产出 + 机器可检查证明」成为标准组合，数学共同体对 AI 结果的信任成本将从「人类数月审稿」降为「机器数秒校验」，同行评审的默认工作流将被重写。

  2. 多 agent 长程任务的成败开关被点名：状态与任务图，而非模型智力。 公告披露早期失败根因是 agent「丢失项目状态、停止协作」，Prove2Me 用 DAG 任务图 + 陈述/证明分离 + 自然语言索引解决。影响判断：这对所有在跑多 agent 工程的团队是可直接迁移的对照实验——任务编排、状态持久化与记忆缓解的优先级应高于堆模型能力，11 天 60 亿 token 的战役级任务已经能靠「编排取胜」。

  3. 1300 万行 / 11 天：形式化的成本曲线被打穿。 社区 blueprint 预期数年，Claude 用 11 天完成；同场实验里三个个人订阅 3 天搞定三素数定理。影响判断：Lean/Mathlib 生态的护城河正在从「人力写证明」切换到「AI 批量生产 + 人力审结构」，任何依赖数学库或形式化资产的团队都应重新评估人力配比。

  4. 对软件工程是隐喻也是预告。 若 LLM 生成的 1300 万行数学证明可以被机器逐行验证，那么 LLM 生成的编译器、协议与安全关键代码没有理由停留在「code review 靠人眼」。影响判断：证明助手与静态验证工具链（Lean、Rocq 及 comparator 这类对齐检查器）会从数学圈外溢到关键软件工程，正确性敏感岗位值得提前 6-12 个月布局。

  5. 科研生态正在被定向灌溉。 Anthropic 与其他实验室近期扩大了对纯数学与形式化方向外部研究者的免费/折扣订阅、研究 credits 与专项 grants，明确把形式化列为「AI 让人无条件感到安心」的用途。影响判断：这是少数 AI 公司主动补贴的学术方向，研究机构申请窗口与算力杠杆现在都处于有利位置。

工程师/产品人今天能做什么

  1. 通读一手材料：读 Anthropic 公告全文，clone anthropics/fermats-last-theorem 仓库，重点看仓库如何组织 1300 万行证明的文件结构与依赖图——这是「AI 大规模产出如何被人接管」的最佳现成标本。
  2. 对照审计自己的多 agent 编排：拿「agent 丢失状态 → DAG 任务图 + 分文件 + 自然语言索引」这条因果链检视现有框架：有没有集中式任务图、失败恢复协议、跨 agent 记忆机制？没有的话先补这三样，再谈提升模型档位。
  3. 跑一个一周内可完成的形式化 PoC：选一条你们领域的中等难度定理（或 Mathlib 中未覆盖的引理），用 Claude Code 类工具 + Lean 试写并让内核校验，记录 token 成本与迭代轮次，建立「AI 产出 + 机器验证」的内部基线数据。
  4. 把「可验证性」写进 AI 代码生成的要求清单：对编译器、加密、支付等正确性关键模块，要求 AI 生成补丁附带不变量或性质测试，并评估引入 Lean/Rocq 做关键路径形式化验证的试点范围与成本。
  5. 若在科研或数学工具产品线：关注 Anthropic 面向外部研究者的免费/折扣订阅与专项 grants 通道，申请额度用于内部形式化或 Lean/Mathlib 贡献，同时把 Prove2Me 类协作模式纳入产品路线图评估。

待观察

  • 社区独立复验尚未完成：Buzzard 的背书与 Lean 内核检查是第一层保证，但 Mathlib/Lean FRO 社区对 1300 万行证明的全面 review、以及对「简化版 Wiles 证明路线」的公认度，仍需数周观察；Buzzard 个人博客的完整长评（当前访问受 bot 防护限制）值得跟进。
  • 可复现性与真实成本：60 亿 token 跑在内部研究模型上，公开模型能否复现、按公开 API 计价的总成本是多少均未披露；Anthropic 是否会发布模型细节或成本白皮书是下一个信号点。
  • 竞赛是否开启：同一窗口 OpenAI GPT-6 Astra 也披露用 Lean 形式化验证解出 FrontierMath 两个开放问题——当两大实验室都押注「形式化」作为 AI 数学的可信通道，下一个被攻克的 landmark 定理（黎曼假设？BSD 猜想？）与独立第三方评测标准值得跟踪。