Axiom Math 借助数十个 AI Agent 完成有限单群分类定理 Lean 形式化并修复历史漏洞

AI 数学公司 Axiom Math 组织数十个 AI Agent 在 24 天内完成了有限单群分类定理的 Lean 形式化，生成约 4310 万行代码与 205 万个形式化声明，代码已开源至 GitHub。