AI 完成有限单群分类定理形式化验证，发现并修复人类证明漏洞

Axiom 团队利用多智能体系统在 24 天内完成了有限单群分类定理的 Lean 代码形式化验证，生成 4310 万行代码。AI 在验证过程中发现人类证明中 34 处逻辑偏差，包括不平衡群定理的关键漏洞。通过与数学家合作，AI 证明了新定理修复了该漏洞，完成了人类史上最大规模的数学证明形式化。