1000 个 Claude 智能体 11 天用 Lean 形式化费马大定理

Anthropic 研究员 Lance Martin 在 AIECode 大会披露：1000 个 Claude 智能体协作，用 11 天完成了费马大定理（Fermat's Last Theorem）的 Lean 形式化。过程中共证明 30,300 个定理，产出 1300 万行 Lean 代码，规模超过 Mathlib 数学库的 5 倍。主智能体在结束时向 main 分支发出冻结指令，并向其余 999 个智能体致谢。该项目的机制是多智能体分工：主智能体拆解证明依赖，子智能体并行证明各层级引理，再逐步合并。对比此前人类团队（如流体动力学问题形式化项目）耗时数月的进度，这次演示展示了大规模智能体协作在形式化数学上的可行路径。