Axiom 团队利用多智能体系统 AxiomProver，在 24 天内完成有限单群分类定理的全面形式化，构建了超 4310 万行的 Lean 代码库，并成功修复了原始证明中的关键逻辑漏洞，标志着 AI 在纯数学研究中实现了从验证到发现的飞跃。