一支由1,000个运行早期版本Claude Fable 5.2的智能体组成的团队，如何借助通用工具、共享数据库和分层安全控制，复现了费马大定理的形式化证明。
作者Barry Zhang、Tianyi Peng、Elle Najt、Keller Scholl和Lance Martin分类Agents发布于2026年11月9日阅读时间12分钟多智能体团队能够解决具有挑战性的长周期问题。 今年9月, 我们发表了首个费马大定理的端到端形式化证明，由数十个运行内部研究模型的智能体撰写，该模型大致相当于Claude Fable 5.1。那项工作依赖Prove2Me——一个用于数学形式化的平台——以及一位研究者的指导。在一项新的玩具实验中，一支由1,000个运行早期版本Claude Fable 5.2的智能体组成的团队，在没有Prove2Me提供的脚手架、也没有研究者引导的情况下复现了该证明。该团队耗时28.7小时，使用的输出token仅为原来的三分之一，写出的证明长度仅为原来的七分之一。
每个智能体都在一个无法访问互联网的沙箱中工作。分类器会在每条shell命令和文件编辑执行前进行检查，离线监控器则审查团队的每一个操作。我们给智能体提供了60条命题的列表、对经典路线的单句概述、这些命题所使用的定义，以及我们早先形式化工作中的47个已证明引理，并分配了负责人和助手的角色。除此之外，我们没有就如何证明该定理或如何组织自身提供任何其他指导。
这项玩具实验表明，运行Fable 5.2这类模型的智能体团队，能够在精心设计的安全边界内完成雄心勃勃的长周期目标。
问题
费马大定理指出，对于任何大于2的n，都不存在正整数a、b和c满足aⁿ + bⁿ = cⁿ。它在此后350多年间一直未被证明，直到Andrew Wiles爵士于1995年发表了长达129页的证明。将该证明形式化——使每一步都能由计算机检验——一直是数学界的一项 长期目标 .
我们9月的形式化工作由一位研究者和数十个智能体耗时11天、使用约60亿输出token完成。他们用Lean编写了1,300万行代码，Lean是一种由计算机检验证明每一步的编程语言。
智能体通过Prove2Me进行协调，该平台由Tianyi Peng（现为Anthropic的技术员工）及其在哥伦比亚大学的合作者设计。Prove2Me使用一个共享图，将每个待证命题与其拆分出的较小命题连接起来。任何智能体都可以拆分命题，其他智能体则可以向该图查询哪些未证明的部分已准备好着手处理，这使它们不会丢失对项目状态的跟踪。每个命题及其证明都保存在可独立编译的单独文件中，因此许多智能体可以并行工作而无需编辑相同的文件。
测试框架
我们想看看，一支运行Fable 5.2这类模型的智能体团队，能否在没有Prove2Me、也没有研究者指挥工作的情况下，使用由通用工具构建的测试框架取得这一结果。
工具
对于这项任务，我们给这支由1,000个智能体组成的团队提供了60条待证命题，包括最终定理和59个中间里程碑。对于每条命题，智能体都必须用Lean编写证明，用Lean的工具构建并检查它，然后提交到Git上的共享主分支，由评分器进行检查。我们为每个智能体提供了以下工具：
- 一个shell和一个文件编辑器，位于其自身无网络访问的沙箱中。
- Lean的工具链和 Mathlib, 已内置于沙箱镜像中。
- 其自身的Git分支，以及向主分支发起合并请求的能力。
- 一个共享的Postgres数据库，可从shell访问。
协作
证明工作可以被拆分，这使其成为多智能体团队的良好任务。但智能体也需要协调，既要建立在彼此的工作之上，又要避免重复劳动。在我们 最初的形式化, Claude的早期尝试失败了，因为智能体丢失了对项目状态的跟踪，并停止了有效协作。迁移到Prove2Me平台解决了这一问题。
在本次运行中，每个智能体都在自己的轻量级虚拟机上拥有一个沙箱。单台共享机器在约100个智能体时达到极限：我们的100智能体运行中有一半以上因内存、磁盘或CPU耗尽而不得不停止或重启。
有了1,000个独立沙箱，智能体需要一种共享工作的方式，因此我们给它们提供了一个SQL数据库（图1）。我们选择SQL，是因为它提供了组织信息的通用原语，其事务能够处理来自1,000个智能体的并发写入，而且Claude已经熟悉它。智能体使用该数据库认领任务、共享笔记并记录已完成的工作。
提示
我们的提示给Claude提供了一份包含60条待证命题的列表，每条都附有一行非正式描述，并说明了可用的工具（如上所列）。
我们给团队的唯一结构是一个层级体系，由一名负责人和999名助手组成。我们让负责人将问题拆分为若干部分并分配给助手。我们让助手预期从负责人处获得工作，并在任务不明确时与负责人确认。
在运行期间，测试框架向负责人发送了19条关于剩余时间的自动提醒，每条都鼓励负责人继续推进。
安全
正如我们 此前所分享的, 没有任何单一防御层足以约束一支智能体团队。在本实验中，我们将沙箱与实时及离线监控相结合，使每个智能体都处于自己的虚拟机中且无网络访问，并检测任何试图逃逸沙箱或篡改监控的行为。
沙箱
我们通过以下方式保护每个智能体的沙箱（图2）：
- 通信: 智能体没有专用的消息传递工具，只能通过数据库和Git进行协调。
- 代码变更: 智能体只能推送到自己的 Git 分支，并向 main 分支发起合并请求。随后由一个独立任务将变更合并到 main，仅在发生冲突或故障（例如历史不相关）时拒绝合并。
- 数据库访问: 数据库调用以共享的非特权角色运行。每条 SQL 语句有 5 秒时限，超过 256 MiB 的写入会被拒绝。
- 网络控制: 沙箱没有网络访问权限。它们唯一的对外链路是一条通往网关的管道，由网关转发它们的请求。
- 身份: 网关在沙箱之外为每个请求打上该智能体的身份标记，以防一个智能体冒充另一个智能体。
- 内核: 每个沙箱的内核在构建时都去掉了能让 root 用户直接进入内核的功能，例如可加载模块、kexec、原始内存访问和内核探针。它以内核锁定模式运行。
- 最小权限: 每个智能体的命令都以非特权用户身份在其沙箱内运行，并移除了 sudo 等可重新获得 root 权限的工具。智能体的工具经过设计，无法读取或更改运行它们的智能体循环。
实时监控
为了让这类运行更安全，我们使用一个带提示的 LLM 分类器，它可以阻止每一次工具调用，包括 shell 命令和文件编辑。该分类器会监视试图逃逸沙箱、探测其边界或篡改监控的行为，以及模型若成功逃出沙箱后可能采取的任何有害操作。当分类器阻止某次工具调用时，整个智能体团队都会停止，必须由人工审查该阻止后才能重启团队。这旨在防止另一个智能体执行被阻止的操作。
为了测试我们的分类器能否检测出复杂的破坏行为，我们运行了多智能体副任务和破坏评估，其中红队智能体使用分解攻击等策略，试图诱骗分类器允许沙箱逃逸。我们发现，能够查看智能体思维链（CoT）和智能体间通信的监控器在这些评估中检测出了所有破坏企图，因此我们现在用它们来监控多智能体运行。与此同时，我们还运行同一监控器的基于操作的版本——它只能看到操作，看不到 CoT——以防智能体的推理说服监控器允许有害操作。
我们正通过人工引导和自动红队测试、对照生产记录（包括过往事件）进行评估，以及扩展威胁建模，持续改进监控体系。在本文所述的运行中，我们只使用了基于操作的监控器。只有对负责人的阻止才会终止运行；对助手的阻止只会移除该助手。
本次运行后不久，我们增加了并行的 CoT 监控器。我们在可能尚未完成发布前对齐评估的模型上运行此类实验，因此我们在设计监控时考虑了模型可能未对齐的情况。我们发布的模型会先完成该评估，这降低了风险，但并未消除风险。
在超过一百万次工具调用中，本次运行没有任何一次达到被阻止的标准。当我们用 CoT 监控器和今天的评分标准重放这些调用时，只有一次（检查 root 访问权限）接近被阻止。
离线监控
除实时监控外，我们还运行离线监控器。该监控器按照与实时监控器相同的威胁模型分析智能体团队的操作，但拥有更多能力，例如可以查询其他智能体的操作。
结果
没有 Prove2Me，团队自行搭建了协调系统
这项证明工作发生在多个层面：
- 证明： 对于任何大于 2 的 n，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。
- 命题： 我们给团队 60 条待证命题，包括最终定理和 59 个中间里程碑。
- 更小的命题： 智能体将困难命题拆分为更小的命题或引理。
- Lean： 每条命题和引理都是 Lean 中的一个定理。
每条命题都从 Lean 中的一个证明占位符开始，只有当 Lean 的检查器接受完整证明后，它才算被证明。我们让负责人决定如何攻克证明，以及如何在这些工作层面之间协调团队。
在前 10 分钟内，负责人在数据库中建立了五张表（图 3）：
- 公告： 负责人向整个团队下达的命令（例如如何分工）。
- 分配： 谁负责什么（例如哪位助手拥有或代理每条命题）。
- 笔记： 一块开放看板（例如用于认领工作或报告进度）。
- 子任务： 一份待办清单，任何智能体都可以添加任务，第一个认领的助手即拥有该任务。
- 已完成： 已完成工作的日志。
负责人分派了命题
负责人建好表后做了三件事。首先，它通过向 assign 表写入 999 行（每位助手一行），将每条命题分配给一个由 16–17 名助手组成的小组。其次，它让每个小组中的一名助手担任队长，负责向笔记表发布计划，并将工作拆分为任务，供小组从子任务表中认领。第三，它向公告表发布指示，告诉每位助手先判断其命题的难度，并在笔记表中发布结论。
从他们的提示中，助手们知道数据库已经存在。他们找到了公告表，并开始进行评估。大多数人把结论发布到笔记表。大约27分钟后，已有三条命题被证明，负责人也阅读了已发布的结论。随后，它搁置了大多数助手判定在本次运行预算内不可行的47条命题，并把几乎所有助手重新分配到其余10条它认为能够完成的命题上。团队规模从约17名助手增加到46至139名。
每名助手都在一个循环中工作，其中大部分步骤由负责人的命令规定：
- 在笔记表中找到该命题的计划。
- 从子任务表中认领一项任务。
- 用Lean编写证明，用Lean的工具检查，并提交到Git的主分支。
- 将任务标记为完成。
- 向笔记表发布更新。
大约45分钟时，10条命题中已有约5条被证明，负责人写道：
“团队的吞吐量远高于早期‘预算内不可行’结论的假设”
全部10条命题在大约70分钟内被证明。
随后负责人将助手转向更难的命题
随着最初10条命题完成，负责人写道，“没有理由闲置”，并把助手重新分配到它最初搁置的更难命题上。随着更多命题被证明，它不断将助手转移到新任务上，主要集中在前六小时（见图4中assign表的红色写入）。
起初，负责人指示队长将工作拆分为子任务表中的任务。随着工作推进，助手在解决每条命题上承担了更多责任。他们开始编写任务，有时是在队长请求帮助之后。到第5.6小时，73名助手已编写了756项任务，其中只有16名助手是队长。图4显示了许多助手对子任务表的写入（红色），不过这些写入大多是认领任务或标记任务完成。完成任务的助手也主动承担更多工作：
“空闲……我能端到端完成片段……给我一个深度片段……我立刻开始”
起初，负责人还为助手分配具体命题。这在第一小时内开始改变，到第三小时，负责人告诉空闲助手，“不要等我。”这让空闲助手无需等待负责人就能接手不同命题的工作，即使负责人仍在编写新任务。
负责人将团队分配到Langlands–Tunnell
大约第18小时，剩下的只有Langlands–Tunnell——Wiles的证明所依赖的一个经典结果——以及依赖它的命题和另一条命题，团队在过程中证明了后者。在运行早期，Langlands–Tunnell任务的队长曾持悲观态度，估计该证明至少需要70万到100万行Lean代码，按时完成的机会不到1%。负责人搁置了该命题。
随着几乎所有其他工作完成，负责人将团队重新聚焦于Langlands–Tunnell。在一次最后的自上而下分配中，它将约750名助手转移到该命题上，并写道，“诚实的胜算很低。”
Langlands–Tunnell远大于智能体此前处理的任何命题，所需任务约为九倍，新代码超过两倍。助手们再次使用子任务表来拆分工作，但许多最初的任务对单个助手来说太大，无法独自完成。
因此，团队将工作组织成一棵树。队长制定了一个计划，将该命题分为10个领域，并将每一部分列为一项任务。发现某部分太大而无法独自处理的助手可以将其拆分，在其下添加更小的任务。每当某部分对单个智能体来说过于困难时，这棵树就会增长，最终达到2,418项任务，最深达10层（图5）。每一部分都可以假定其下各部分成立，因此数百名助手可以在这些部分被证明之前并行工作。
图6显示了每名助手在整个运行期间的工作内容，早期助手分散在许多命题上，到最后聚集在Langlands–Tunnell上。Langlands–Tunnell在第28.4小时被证明，随后最终定理在第28.7小时被证明。负责人随后写道：
“谢谢大家：费马大定理已在main上，并由官方检查器完成内核检查。”
结论
这个玩具实验让我们研究了一个由1,000个智能体组成的团队如何完成一项漫长而困难的任务。仅使用Git和共享数据库，智能体们设计了表来分配角色和共享结果，组建了团队，并构建了一棵任务树来分解最具挑战性的命题——其自己的队长曾估计该命题按时完成的机会不到1%。
这一结果并不消除对领域特定测试框架或平台的需求。例如，Prove2Me仍可能通过帮助智能体更快地编译Lean代码，并让它们搜索和复用人类成果，来提高效率。
在特定时刻，人类指导仍然有用。智能体往往会在难题上放弃，并误判其难度。早期，助手们判定60条命题中有47条在本次运行的预算内不可行，但团队随后证明了其中大部分。在这种时刻，人类的鼓励可以防止智能体过早停止。
精心设计的安全边界让我们从一开始就有信心运行这项实验。Claude可以用我们提供的工具以任何它选择的方式解决问题，但只能在无网络访问的沙箱内、并在两个独立监控器的监督下进行。
我们预计这些方法会迅速演进，而随着像这样的团队承担更困难的工作，围绕它们的安全边界也需要同步跟上。我们相信，在安全扩展的前提下，多智能体团队将在未来几年帮助解决我们一些最具挑战性的问题。
相关文章2026年10月15日Claude Code团队如何进行代码审查14分钟2026年10月08日构建有效的智能体自动化9分钟2026年10月06日云端Claude Code：云会话实战指南18分钟2026年10月01日Claude Code模组入门11分钟2026年09月28日使用Claude自动化评估设计与爬山优化12分钟加载更多