1637 年，费马在他那本《算术》的页边写下了一句著名的”挑衅”：他发现了 n>2 时 aⁿ+bⁿ=cⁿ 无正整数解的美妙证明，可惜”页边空白太窄写不下”。此后 350 多年，无数数学家在这句话上折戟——1908 年悬赏 10 万金马克（相当于今天的百万美元级），光是第一年就收到 621 份错误证明。
1995 年，安德鲁·怀尔斯用 129 页完成了证明。但这远不是故事的终点：验证这份证明，数学界又花了数年。而现在，9 月 4 日 Anthropic 官宣了一个让数学界震动的结果——Claude 用 11 天，把费马大定理变成了机器能逐行核对的东西。
发生了什么：不是新证明，是”机器可查”的证明
先厘清一个关键区别，否则容易被标题误导：Claude 没有发现费马大定理的新证明，定理本身仍是怀尔斯的成果。Claude 做的是形式化验证——把已有的数学推理翻译成 Lean 证明助手能逐行机械检查的代码，每一步都只能依赖公理和已被证明的定理，不允许”此处略去”。
Anthropic 公布的数字相当惊人：
- 11 天，基本自主完成，几十个 Claude Agent 并行协作
- 1300 万行 Lean 代码，相当于 Lean 最大社区库 Mathlib 的 5 倍以上
- 证明约 3.03 万个定理，其中 2.95 万个直接用于最终证明
- 全程消耗约 60 亿输出 token
- 最终只依赖 Lean 的三条标准公理，无 sorry 占位、无隐藏假设
外部数学家、帝国理工学院的 Kevin Buzzard 独立复核了这份成果——他本人正是牵头用 Lean 形式化费马大定理社区计划的人（他自己的仓库到现在还是”施工中”）。Buzzard 的评价是：这是”非凡的自动形式化成就”，证明”除了数学公理外不依赖任何假设”；如果费马大定理级别的自动形式化现在可行，”我们就在现代数学文献自动形式化上迈出了一大步”。
为什么验证这么难：怀尔斯自己就栽过跟头
费马大定理的验证难度，从怀尔斯的经历就能看出来。1993 年 6 月，他做了三天讲座宣布证明完成，结果两个月后，一位审稿人问了个问题，暴露了论证里一个致命缺口。怀尔斯独自修了一年几乎放弃，最后靠和学生理查德·泰勒合作，才在 1995 年补上漏洞正式发表。
这个故事说明数学验证的本质：一条逻辑链只要有一环是松的，整座大厦就可能塌。人工审稿靠的是”论证令人信服”，而机器验证要求”每一步都被证明助手检查过”。人类想弄懂一个新结果、确认它没错，常常要数月甚至数年；而 Claude 这次展示的路径是——AI 负责产出，Lean 负责逐行核对，人负责理解思路和把关方向。
怎么做到的：几十个 Agent 并行 + 一张共享”证明地图”
真正让这次突破成立的不是模型变聪明了多少，而是一套工程机制。
Anthropic 没有让单个 Claude 闷头干 11 天，而是让几十个 Agent 分工并行：有人定义数学概念，有人证明中间定理，有人基于已完成的结果继续推进。这么多 Agent 协作最大的坑是状态丢失——Anthropic 透露，第一轮尝试确实失败了：没有协调机制时，Agent 会互相遗忘进度、重复造轮子，最后协作崩盘。
破局工具叫 Prove2Me，由 Anthropic 研究员田天意（Tianyi Peng，哥伦比亚大学）团队设计。它维护一张所有定理的”依赖图”，每个 Agent 都能看到什么已证明、什么还缺、各部分怎么衔接。配合 Claude Code 的多 Agent 工作方式，复杂证明被拆成可并行的小目标，谁都不用重复推导同一个引理。Claude 也不是从零开始：它站在 106 个社区既有文件（包括 Buzzard 团队的弗雷曲线、伽罗瓦表示等基础工作）之上，沿现代版怀尔斯论证路线推进。
顺带一提，Anthropic 还披露了一个配套实验：用消费级 Claude Max 订阅，3 天完成了另一个著名数论问题（维诺格拉多夫三素数定理）的形式化——也就是说，这条路正在从实验室走向普通用户。
对数学和 AI 意味着什么
往小了说，这是给数学界递了一件工具：过去一个复杂证明从发表到被放心引用要耗数年人力，今后 AI 形式化可以把核验周期压到天级别。往大了说，Anthropic 的设想是未来数学论文可能”双轨”发布——一份给人读的叙述，一份给机器查的形式化证明。这不会取代数学家的创造力，但会改变成果被验证和传播的方式：提出新理论的人，可能同时要负责让理论能被机器理解。
对做 AI 的人，这件事还有另一层参照。上周刚写过 Claude Code 一次”安全审查”删掉 700GB——AI 越主动越可能闯祸，单靠模型自夸”我检查过了”并不可靠。费马大定理这次的价值恰好相反：它示范了一种”AI 产出 + 独立机器校验”的范式——AI 负责规模和速度，形式化系统负责正确性，两者解耦。这套范式如果跑通，意义远不止数学。
老达点评：里程碑不在”证明”，在”验证的可扩展性”
我的判断是，别只盯着”11 天”这个博眼球的数字。真正的信号是验证成本的结构性下降。数学界苦人工验证久矣——开普勒猜想审了多年只能给”高度可信”，佩雷尔曼的庞加莱猜想让同行整理了多年。当 AI 能批量产出数学成果，人类逐一阅读验证将更加不现实，形式化验证几乎是唯一出路。
而这件事能成，靠的恰恰是我在 Claude 专题 反复讲的判断：前沿模型的比拼正从”单次对话能力”转向”长程多 Agent 协作的可靠性”。Claude Code 默认模型换 Fable 5.1 时那套 1M 上下文、长任务能力，在这类 AI 智能体与自动化 场景里才是真正的用武之地——上下文装得下整个证明地图，Agent 才能不丢状态地协作十几天。
当然也要泼盆冷水：这是验证已知定理，不是发现新数学；是 Anthropic 自述 + 一位外部复核人，尚无第三方独立复现。但方向已经很清楚——数学家以后要同时面对人和 AI 了，而 AI 的产出，从此可以真正被”查账”。
