Axiom 多智能体系统24天完成有限单群分类定理的 Lean 形式化

Axiom 团队的 AxiomProver 多智能体系统用24天完成了百余名数学家历时半个世纪写成的15000页有限单群分类定理（CFSG）的形式化验证，产出4310万行 Lean 代码。