AI agent 集群 24 天形式化 15000 页证明,Axiom 攻克「巨大定理」

rickasaurus · x · 2026-10-28

Axiom 发布有限单群分类定理(CFSG)的完整 Lean 形式化——史上最长的数学证明,约 15000 页、500+ 篇论文、约 100 位作者,如今约 3800-4000 万行 Lean 代码,由数十个 AI agent 组成的集群在 24 天内写成,数学家和工程师负责引导。关键对比:今年年初,让 AxiomProver 写出正确的 1 万行 Lean 证明还需数周调教,如今 agent 集群完成了约 4000 倍规模的工作。Axiom 将这一飞跃归功于同时重建三层:模型、harness 与基础设施。该项目还在文献中发现约 100 处实质性修正,被视为「可验证 AI」的标志性进展——形式化数学开始像软件一样规模化。