费马在书页边写下那句「我有一个绝妙的证明，可惜空白太小写不下」之后，数学家们等了 350 多年，才等到安德鲁·怀尔斯在 1995 年给出 129 页的完整证明——而验证这个证明本身，又花了数学界数年时间。把怀尔斯的证明「翻译」成机器能逐行检查的形式化证明，更是一个被预估要以年为单位的长期工程。
9 月 4 日，Anthropic 官宣了一个让数学界侧目的结果：Claude 在 11 天里，基本自主地完成了费马大定理的端到端机器可校验证明——几十个智能体协作写下了约 1300 万行 Lean 代码，证明了 3 万多个中间定理，整个过程只有少量高层人工指导。这不仅是数学形式化的一次飞跃，更是多智能体长时协作迄今最硬核的一次工程演示。本文把这件事的事实、它怎么做到的、以及为什么它对做 Agent 的人同样重要，一次讲透。
事实梳理一：11 天、1300 万行、3 万定理——数字背后是什么
先看关键事实：Anthropic 研究员 Tianyi Peng 原本只是想测试 Claude 能否推进社区的形式化工程，结果远超预期。Claude 沿用了怀尔斯证明的现代简化版本（Frey-Serre-Ribet-Wiles 路线），在 11 天内：写下了约 1300 万行 Lean 代码——规模是 Lean 核心数学库 Mathlib 的 5 倍以上；构建了约 30300 个机器可验证的定理证明，其中约 29500 个进入最终证明；整个过程消耗约 60 亿输出 token，运行在一款能力接近 Claude Fable 5.1 的内部研究模型上。人类的数学输入很少：Peng 偶尔给出「雅可比簇作为概形的优先级很高」「尽快完成 Mazur 定理」这类方向性提示，具体推导基本由 Agent 推进。
验证环节同样关键：最终证明通过了 Lean 内核检查，只依赖 Lean 的三条标准公理，没有任何「假设成立」的占位；比对工具还确认了 Claude 所证定理的表述与 Mathlib 中的费马大定理陈述一致。帝国理工学院数学家 Kevin Buzzard——正是 2024 年发起 Lean 社区形式化工程、原计划做到 2029 年的人——审阅后评价这是「非凡的自动形式化成就」。换句话说，这不是 AI 自说自话，是独立软件逐行检查过、领域权威认可的机器证明。
事实梳理二：几十个 Agent 是怎么协作 11 天不跑散的
这件事对 Agent 圈最有价值的不是数学，而是工程：几十个智能体并行协作、持续 11 天、中途不散架，靠的是什么？Anthropic 自己披露了关键细节——一开始并不顺利。早期实验里，多个 Claude 智能体很快失去对全局进度的掌握：不知道哪些命题已经完成、难以复用彼此的结果，协作随之停滞，最终证明里约 7% 的非模板代码仍来自这些失败尝试。
转折点是一个叫 Prove2Me 的开放协作平台（Peng 与哥伦比亚大学合作者开发）：它把待证明的定理组织成一张有向无环图，每个节点是一项任务，节点之间记录依赖关系——智能体据此判断下一步该证什么，也能在长时间运行后重新找回当前进度；平台把定理陈述与具体证明拆分到不同文件、独立维护连接，缩短 Lean 编译时间；每个定理还配自然语言描述，方便智能体搜索和复用已有结果。一句话：Prove2Me 给几十个 Agent 提供了「共享的任务地图和进度记忆」，这正是 多 Agent 协作 最容易翻车的地方——任务怎么拆、上下文怎么共享、进度怎么同步，它用一张依赖图全解决了。
影响分析一：对数学界——「验证」正在从人评变成机器可查
需要澄清的是：Claude 这次没有提出新的证明路线，它做的是把已有证明「形式化」——把自然语言推理转写成机器可逐行核验的代码。但这个「验证环节的自动化」意义重大：数学论文依赖同行评审，而面对越来越复杂的证明，人工评审越来越吃力——开普勒猜想评审花了好几年，庞加莱猜想的确认同样旷日持久。当 AI 生成数学成果的速度远超人类审稿能力时，形式化证明提供了第三条路：AI 负责生成、人类负责理解思路、Lean 这类证明助手负责检查逻辑。Buzzard 的结论是：如果费马大定理都能自动形式化，那距离「整个现代数学文献都可机器核验」就不远了。未来数学论文很可能同时存在两套表述——一套给人类读的「思路版」和一套给机器查的「形式化版」。
影响分析二：对 Agent 行业——长时协作的「脚手架」比模型更重要
这次演示最硬核的一点是任务规模：1300 万行代码、3 万定理、11 天，远超普通编码任务的体量。它验证了一个我们站上反复讲的观点——Agent = Model + Harness：模型能力决定单个任务能走多远，但几十个 Agent 能否围绕同一目标持续协作数天，决定权在 Harness 层。Prove2Me 就是 Harness 的极致样本：任务依赖图（编排）、进度状态管理（记忆）、自然语言检索（上下文）、文件拆分（性能优化），每一层都在补模型的短板。这也回应了 AI Agent 长时任务 设计里反复强调的一点——长任务不是「让模型一口气干完」，而是「把任务拆成可并行、可校验、可恢复的单元，再配一张进度地图」。想做长时多 Agent 任务的团队，Prove2Me 的任务图设计值得直接抄作业。
影响分析三：对普通团队——门槛正在快速下降
Anthropic 还做了一个更小的实验：用三个个人版 Claude Max 账号，通过 Prove2Me 协作，只花三天就完成了维诺格拉多夫三素数定理的形式化。这个信号很关键：说明这类工作未必局限于大型实验室——只要任务拆解和协作机制足够成熟，普通研究团队甚至个人订阅用户也能参与数学形式化。对于做 Agent 的人来说，这意味着两件事：一是「多 Agent 长时协作」的工程方法正在从论文走进开源工具，多 Agent 编排 的实践门槛会越来越低；二是当 Agent 能产出越来越难人工核验的成果时，「如何让成果可被机器核验」本身会变成一种核心竞争力——这和 AI Agent 评测 里「用数据而不是感觉判断 Agent 好坏」是同一个逻辑的极致版。
老达点评
第一，别被「证明费马大定理」这个说法带偏，它不是 AI 攻克了未解难题，而是 AI 把「验证」这件苦差事做到了人类做不到的规模。费马大定理早就被怀尔斯证明了，Claude 的贡献是把验证过程机器化——这反而更值得尊敬，因为数学界真正的瓶颈早已从「证明」转移到「验证」。对做 Agent 的我们，这是个提醒：AI 生成内容的能力越强，「怎么证明 AI 没搞错」就越值钱。别只盯着让 Agent 干更多活，要同时给它的成果配上「机器可核验」的通道——证据包、回放、结构化校验，都是在业务里做「Lean 内核」。能力越强越要门控，这个判断在数学和商业里通用。
第二，这次「先失败、后成功」的披露，含金量比结果本身还高。Anthropic 没有把 11 天包装成一路顺风，而是承认早期实验里 Agent 协作失序、丢了全局进度。这个失败案例恰恰点出了多 Agent 系统的真问题：不是模型不够聪明，而是没有共享的任务地图，再聪明的 Agent 也会各干各的。Prove2Me 的价值不在算法而在架构——把任务依赖、进度、上下文这些「软状态」变成显式的「硬结构」。做多 Agent 应用的团队，先问自己一句：我的 Agent 们知道彼此干到哪了吗？如果不知道，模型再强也会跑散。
第三，关于「AI 数学」的边界，我的判断是：形式化会率先成熟，新发现还需要时间。Claude 这次是「翻译并核验」已有证明，而不是提出新证明思路——这符合预期，因为提出新思路需要的是数学直觉，而形式化需要的是「把直觉变成可检查的步骤」，后者正是大模型当前最擅长的事。未来几年更可能看到的是：AI 大量参与已有数学成果的机器核验、帮人类发现现有证明中的漏洞；至于 AI 独立提出并证明全新猜想，那会是更后面的事，别急着下结论，也别急着神话。
第四，三个 Max 账号三天证明三素数定理——这是今年我看过「Agent 民主化」最好的注脚。当一项昨天还需要大实验室几十个 Agent、60 亿 token 才能做的事，今天三个订阅账号就能做到入门版，说明这类能力的边际成本在断崖式下降。对普通团队的建议很实在：别等「完美的多 Agent 平台」，先把一个真实任务拆成依赖图、配上进度记录跑起来——AI Agent 工作流设计 的方法现在就能用。工具会越来越便宜，先跑起来的人先积累经验。
总结
Claude 用 11 天、1300 万行 Lean 代码、3 万多个中间定理，完成了费马大定理的端到端机器可校验证明——数学上，它把「验证复杂证明」从数年人工评审压缩到两周机器检查；工程上，它用 Prove2Me 的任务依赖图解决了几十个 Agent 长时协作的失序问题，给所有做多智能体的人上了一课：共享的任务地图，比单个 Agent 的聪明更重要。老达点评：别神化「AI 证明定理」，它真正示范的是「AI 成果如何被机器核验」——在数学里是 Lean，在业务里就是证据包和回放；先失败后成功的披露说明多 Agent 的瓶颈在架构不在模型；形式化会先成熟、新发现还需要时间；而三个订阅账号三天跑通三素数定理，意味着这套能力正在快速民主化。热闹在数学界，功课在 Agent 圈——把任务编排和成果核验做扎实，下一次「11 天奇迹」可能就是你的业务。
