Axiom Math 数十个 AI Agent 用 24 天形式化有限单群分类定理并发现近 40 年的漏洞

Axiom Math 宣布，数十个 AI Agent 在 24 天内完成有限单群分类定理的 Lean 形式化，生成约 4310 万行代码和 205 万个形式化声明，并给出覆盖整个分类定理的计算机检查证明。工程将分散在 500 多篇论文中的推理组织成可逐步检查的形式系统。过程中，Agent 还发现一处存在近 40 年的历史论证漏洞，并参与构造一项新的群论结果。