发表机构
Kansas State University（堪萨斯州立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究在 Lean 中构建了一个有限单群的构造性图册，覆盖八个族和十五个零星群，证明其阶、单性及结构性质，并形式化模型以供验证和重用。
AI 中文摘要
我们呈现了一个有限单群的构造性图册，其中包含其阶、单性和结构性质的证明。已完成的八个族是素数阶循环群、交错群、经典系列 $A_r(q)$、$B_r(q)$、$C_r(q)$、$D_r(q)$，以及例外系列 $G_2(q)$ 和小型 Ree 群 $ {}^2G_2(3^{2m+1})$，其中 $m\geq1$。十五个零星条目是 $M_{11}$、$M_{12}$、$M_{22}$、$M_{23}$、$M_{24}$、$\mathrm{Co}_1$、$\mathrm{Co}_2$、$\mathrm{Co}_3$、$\mathrm{McL}$、$\mathrm{HS}$、$\mathrm{Suz}$、$J_2$，以及 $\mathrm{Fi}_{22}$、$\mathrm{Fi}_{23}$、$\mathrm{Fi}_{24}'$。简单的参数范围和例外情况被明确陈述。这些模型来源于编码、格、形式、代数和有限几何，包括分裂八元数和 Conway--Parker 代数。它们保留了自然作用、稳定子、中心商以及用于后续群论的比较映射。几个经典比较同构关联了这些模型，而对合类计数区分了奇特征且秩至少为三的等阶正交族和辛族。借鉴经典文献和配套的数学工作，该项目发展了有限单群理论的构造方面，而非分类的穷举性证明。已完成的模型和陈述的证明在 Lean 中形式化，以便验证和重用。
英文摘要
We present a constructive atlas of finite simple groups with proofs of their orders, simplicity, and structural properties. The eight completed families are cyclic groups of prime order, alternating groups, the classical series $A_r(q)$, $B_r(q)$, $C_r(q)$, $D_r(q)$, and the exceptional series $G_2(q)$ and the small Ree groups $ {}^2G_2(3^{2m+1})$, $m\geq1$. The fifteen sporadic entries are $M_{11}$, $M_{12}$, $M_{22}$, $M_{23}$, $M_{24}$, $\mathrm{Co}_1$, $\mathrm{Co}_2$, $\mathrm{Co}_3$, $\mathrm{McL}$, $\mathrm{HS}$, $\mathrm{Suz}$, $J_2$, and $\mathrm{Fi}_{22}$, $\mathrm{Fi}_{23}$, $\mathrm{Fi}_{24}'$. The simple parameter ranges and exceptional cases are stated explicitly. The models arise from codes, lattices, forms, algebras, and finite geometries, including the split octonions and the Conway--Parker algebra. They retain natural actions, stabilizers, central quotients, and comparison maps for subsequent group theory. Several classical comparison isomorphisms relate the models, while involution-class counts distinguish the equal-order orthogonal and symplectic families in odd characteristic and rank at least three. Drawing on classical sources and companion mathematical work, the project develops the construction side of finite simple group theory, not the exhaustiveness proof of the classification. The completed models and stated proofs are formalized in Lean for verification and reuse.
Comments29 pages. Lean formalization, catalogue, and verification material available from the source repository linked in the paper
