有限单群可以理解为有限对称结构的基本构件；分类定理说明这些构件属于哪些家族，以及 26 个例外的散在群。其已有证明散布在大量论文中，读懂局部论证不等于能确认整条依赖链。Axiom 宣布用 Agent 将这套庞大证明转写为 Lean 形式：每个推理步骤都必须符合证明助手的规则，再由其内核检查。团队报告 24 天生成约 4310 万行 Lean 代码；这是项目自报的工程规模，不是我们独立重建后的结论。
方法先把证明组织成里程碑和任务图，再让不同 Agent 处理局部证明，专门整合定义、引理和依赖。已有 Mathlib 与清华求真书院形式化工作提供基础。这里容易失败的地方不是某条公式算错，而是两个局部团队给“同一个对象”用了不兼容定义，或为了证明方便悄悄加了更强前提。原文说整合时因此删除了大量不可直接接入的代码。
团队列出 34 处值得注意的原论证偏差。例如，不平衡群定理（UGT）用子群信息识别整体，其中一个证明步骤假定某种操作后的对象仍留在指定类别；Agent 找到反例，团队于是改走另一条证明路径。不能把这写成“有限单群分类被推翻”：需要区分定理、证明中的某个步骤及其修补。公开工程把许多此前依赖人工信任的环节变成可检查对象，但形式化命题是否准确表达原数学含义，仍需要人审阅。