Claude 用 11 天把费马大定理写成 Lean 4 可检查证明，这件事比“AI 会做数学题”更硬：它把数学结果放进了一个机器能逐行验收的系统里。
我的判断是，这条新闻的重点不在天才感，而在复核成本。过去大模型做数学，常见问题是答案看起来漂亮，推理链却很难追责。Anthropic 这次公布的不是一段聊天记录，而是一个 GitHub 仓库、一条证明路线、Lean 内核检查、comparator 对照检查，以及 nanoda 第二套内核接受同一环境的记录。
热闹在“证明”，门槛在“检查”
Anthropic 说，Claude largely autonomously 工作 11 天，生成了 1300 万行 Lean，证明了 29500 个中间定理，最终得到首个端到端、计算机检查过的费马大定理证明。仓库 README 里的说法更克制：这是一个 research artifact，不维护，也不接受贡献。这个提醒把热度拉回了正轨：它是研究样品，不是可以直接外包数学判断的按钮。
这个克制很重要。数学界不会因为一个模型宣称“我证明了”就改写教科书。真正能让人往前走的，是证明能不能被独立工具接住。仓库写明，FinalCheck 要求证明只依赖 Lean 的三个标准公理；comparator 确认目标命题与 Mathlib 里的挑战版本一致；nanoda 作为 Rust 写的独立 Lean 内核，也接受了导出的环境。
AI 不是替代审稿人，而是在压缩形式化的苦活
费马大定理早就由 Wiles 证明过。这里的新东西不是数学结论本身，而是把一条极长、跨多个分支的证明搬进形式系统的速度。Imperial College London 的 FLT 项目本来就是多人、长期、开源的形式化工程。Anthropic 这次像是在旁边插进一台很猛的施工机器。
但施工机器不等于最终的信任来源。Lean 项目里的每个名字、每个中间定理是否对应人类数学家心里的那条路线，仍然需要人读。机器能挡住一类错误：类型不对、依赖不清、偷偷加公理、用未完成证明糊过去。机器挡不住另一类错误：某个形式化对象虽然合法，却不是你以为它表达的对象。
这也是我愿意写它的原因。它不是又一个“模型秒杀人类”的标题，而是把 AI 的能力放到一条可审计链路里。成果可以兴奋，验收不能省。
这会改变科研工具的卖点
对普通读者来说，这件事最值得记住的不是“Claude 比数学家强”。更准确的说法是，AI 正在从解题助手变成可复核工程的加速器。它适合处理大量定义搬运、定理连接、依赖清理和失败重试。人类仍然要决定问题值不值得做，证明路线靠不靠谱，形式化边界有没有偷换。
商业上也一样。以后研究型 AI 产品不能只展示漂亮答案，还要展示它能不能把答案交给一个外部检查器。代码有测试，数学有 proof assistant，数据分析有可复现实验。越是高风险知识工作，越不能只靠模型口才。
这条线如果走通，AI 在科研里的位置会更清楚：不是凭一句“我确信”拿走信任，而是把更多工作推进到可以被别人检查的状态。真正的门槛也会从“模型会不会说”转向“它交出来的东西能不能被验”。
消息来源
- Anthropic：Formalizing Fermat’s Last Theorem，https://www.anthropic.com/research/formalizing-fermats-last-theorem
- GitHub：anthropics/fermats-last-theorem，https://github.com/anthropics/fermats-last-theorem
- Imperial College London FLT project，https://imperialcollegelondon.github.io/FLT/
- Hacker News discussion，https://news.ycombinator.com/item?id=49568506
