有限单群分类定理被完整形式化进 Lean，顺带发现了原证明的漏洞

📋 概述

Axiom Math 团队把有限单群分类定理的第一代证明完整形式化进了 Lean，每一步逻辑都过 Lean 内核检查。这项集体成就原本横跨数千页期刊、约百位数学家用几十年写成，结论是每个有限单群必为素数阶循环群、交错群、李型群或 26 个散在群之一。形式化过程中他们还发现了一个实质问题：第一代证明里通往「非平衡群定理」的一条已发表路径用到了一个闭包断言，而他们找到了反例。配套论文给出障碍说明与替代论证，基于 Solomon 1976 年的极大 2-分量理论，关键一步是定理 2.3（单顶的保持）。团队正在与群论学家整理文献勘误。