Axiom 24 天完成有限单群分类定理的 Lean 形式化验证
Axiom Math 宣布完成有限单群分类定理（CFSG）的首个完整机器校验证明。CFSG 绰号「巨大定理」，被誉为对称性的「元素周期表」，原证明横跨约 15000 页、500 多篇论文、由约 100 位数学家历经数十年完成，是公认人类史上最长的数学证明，贡献者 John Thompson 曾因此获相关荣誉。Axiom 用 AI 智能体集群在 24 天内完成形式化验证，产出约 4300 万行 Lean 代码，是迄今规模最大的数学证明机器验证。
已确认
- Axiom 宣布完成 CFSG 的完整 Lean 自动形式化，为首个完整计算机校验证明。
- 原证明体量：约 15000 页、500 多篇论文、约 100 位数学家参与。
- 形式化耗时 24 天，产出约 4300 万行 Lean 代码。
- 据帖文转述，agent 集群通过 GitHub 协调分工、互相审查，过程中还发现了一个存在数十年的证明缺陷。
为什么重要
- 这是「巨大定理」首次获得逐行机器验证，为数学史上最庞大证明的正确性提供了形式化背书。
- 24 天完成人类数十年积累的证明验证，展示了 AI 智能体集群在大规模协作任务上的能力；有评论者认为这体现了 agent 群体协作模式的潜力。
2026-10-27 ~ 2026-10-28 · 11 条相关
一手来源
- Axiom 用 AI 智能体群完成史上最长数学证明的 Lean 形式化 — kevinweil ·
- Axiom 24 天用 AI agent 集群形式化「巨大定理」，产出 4300 万行 Lean 代码 — rohanpaul_ai ·
- Agent 集群 24 天验证约 1.5 万页数学证明,还揪出十年老缺陷 — cneuralnetwork ·
- 约 1.5 万页有限单群分类定理完成 Lean 形式化，史上最大数学证明获机器验证 — eptwts · 2026-10-27
- 【源头】Axiom 用 AI 智能体群完成史上最长数学证明的 Lean 形式化 — kevinweil · 2026-10-27
- 【源头】Agent 集群 24 天验证约 1.5 万页数学证明,还揪出十年老缺陷 — cneuralnetwork · 2026-10-27
- 巨著定理被完全形式化，数学形式化再下一城 — IgorCarron · 2026-10-27
- 迄今最大 Lean 代码库诞生，Szegedy：ABC 猜想若仍无法形式化将是明确信号 — ChrSzegedy · 2026-10-28
另有 6 条近重复转述:akorinek · rohanpaul_ai · stevenstrogatz · wellecks · pickover · PlisSergey