原始来源：Axiom 原始研究长文
发现渠道：Hacker News · AI
有限单群可以理解为有限对称结构的基本构件；分类定理说明这些构件属于哪些家族，以及 26 个例外的散在群。其已有证明散布在大量论文中，读懂局部论证不等于能确认整条依赖链。Axiom 宣布用 Agent 将这套庞大证明转写为 Lean 形式：每个推理步骤都必须符合证明助手的规则，再由其内核检查。团队报告 24 天生成约 4310 万行 Lean 代码；这是项目自报的工程规模，不是我们独立重建后的结论。
方法先把证明组织成里程碑和任务图，再让不同 Agent 处理局部证明，专门整合定义、引理和依赖。已有 Mathlib 与清华求真书院形式化工作提供基础。这里容易失败的地方不是某条公式算错，而是两个局部团队给“同一个对象”用了不兼容定义，或为了证明方便悄悄加了更强前提。原文说整合时因此删除了大量不可直接接入的代码。
团队列出 34 处值得注意的原论证偏差。例如，不平衡群定理（UGT）用子群信息识别整体，其中一个证明步骤假定某种操作后的对象仍留在指定类别；Agent 找到反例，团队于是改走另一条证明路径。不能把这写成“有限单群分类被推翻”：需要区分定理、证明中的某个步骤及其修补。公开工程把许多此前依赖人工信任的环节变成可检查对象，但形式化命题是否准确表达原数学含义，仍需要人审阅。
可信度 65 · 重要性 91 · 新颖度 82
技术与主题
Agent 系统 · 推理能力 · formal verification · Lean · theorem proving · Multi-Agent
jonath_laurent
发言者自称 Axiom 团队 MTS，回应如何把各部分形式化证明整合。
忠实转述（非原句）：他指出，最大的整合困难之一是同一个非形式化概念，在不同部分被写成互不兼容的形式定义。这使局部证明接不上，需要专门的整合工作。此说法补充团队实施经验，不能作为外部独立验证。
编辑评读
这项工作的机会不只在“机器写了多少证明”。大型证明过去难以反复改动，因为某个定义变化会牵连数十处论证；显式依赖图和可重复检查可能降低这种维护成本。对自动化研究而言，它提示了一个可迁移设计：任务分解时同时分配接口整合工作，否则局部成功会堆积成全局无法拼接的产物。
这里也有两种不同的正确性。Lean 检查的是形式系统里的结论是否由前提推出；数学家还需判断前提、定义和最终陈述是否对应想证明的问题。Axiom 成员在讨论里特别指出定义不兼容的困难，恰好说明“全部通过检查”之前就需要协调语义。自动化越强，这层工作越不宜被代码量遮住。
目前应把发布的证明、关键偏差说明及可重建性分开阅读。本轮读了研究长文和项目总览，没有完成整个仓库的构建，也没有逐项审阅 34 处修补。因此这里报道的是公开成果与方法线索；其长期价值还要看独立数学审阅和他人实际复用。
需要留意
- 团队宣布完成；本轮未构建完整工程或独立审计所有修补。