A constructive ATLAS of finite simple groups in Lean
Abstract
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 Ar(q), Br(q), Cr(q), Dr(q), and the exceptional series G2(q) and the small Ree groups $ {}^2G_2(3^{2m+1})$, m≥1. The fifteen sporadic entries are M11, M12, M22, M23, M24, Co1, Co2, Co3, McL, HS, Suz, J2, and Fi22, Fi23, Fi24'. 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.
Related
- The Codegree Isomorphism Conjecture for Finite Simple Groups
- Infinitely many finite simple groups of Lie type are not generated invariably by two elements of prime order
- Arithmetic invariants for finite simple and related groups
- On finite simple groups possessing a conjugacy class of size 3p^n
- Co-intersection graphs of nonabelian finite simple groups have diameter two
BibTeX
@misc{hohn2026constructive,
title = {{A constructive ATLAS of finite simple groups in Lean}},
author = {Gerald Höhn},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.35847},
eprint = {2609.35847},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.35847},
}
RIS
TY - UNPB
TI - A constructive ATLAS of finite simple groups in Lean
AU - Gerald Höhn
PY - 2026
DA - 2026/09/25
PB - arXiv
DO - 10.48550/arxiv.2609.35847
UR - https://arxiv.org/abs/2609.35847
AB - 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≥1. The fifteen sporadic entries are M_11, M_12, M_22, M_23, M_24, Co_1, Co_2, Co_3, McL, HS, Suz, J_2, and Fi_22, Fi_23, 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.
ER -