Axiom 用 AI 智能体群 24 天完成 CFSG 的 Lean 形式化

Axiom 宣布用 AI 智能体集群完成有限单群分类定理（CFSG）的首个完整 Lean 机器校验证明。形式化耗时 24 天，产出约 4300 万行 Lean 代码；智能体通过 GitHub 协调分工并互相审查，还发现了一个存在数十年的证明缺陷。原证明横跨约 15000 页、500 多篇论文，由约 100 位数学家历经数十年完成。