Axiom 发布有限单群分类定理 AI 形式化项目， 24 天生成 4310 万行 Lean 代码

Axiom Math 宣布由其数十个 AI Agent 在 24 天内完成了有限单群分类定理的 Lean 形式化，生成约 4310 万行代码和 205 万个形式化声明。这一过程不仅提供了第一份覆盖整个分类定理的计算机检查证明，还发现了包括 1986 年 John Walter 关于不平衡群定理中的漏洞在内共 34 处文献偏差，并辅助构造了新的群论结果以修复证明路径。