Lean 完成有限单群分类定理形式化证明

该项目针对的是第一代证明的形式化工作。在此过程中，研究团队发现已发表的一条通往非平衡群定理的路线中，一个闭包断言存在反例。论文解释了这一障碍，并给出了针对单群情形的替代论证，其基础是 Solomon 1976 年提出的极大 2-分量理论，关键步骤为定理 2.3（简单顶点的保持）。

有限单群分类定理是群论领域长期未解的难题，其原始证明散落在数百篇论文中，总计数千页。传统上，这一证明的完整性依赖于数学家的共识，而 Lean 的形式化将每个推理步骤都交给了机器检查。

新产生的论文《非平衡群定理》（Hexagon 2610.00575，35 页）直接源自形式化项目，属于项目过程中的意外收获。它既修正了原有文献中的缺陷，也展示了形式化方法在发现和修补数学错误方面的实际价值。