{"id":"arxiv/2609.35847","url":"https://arxiv.org/abs/2609.35847","tags":["cs.SC","cs.LO","math.GR"],"score":0,"title":"A constructive ATLAS of finite simple groups in Lean","domain":"cs.SC","source":"arxiv","authors":["Gerald Höhn"],"reviews":0,"subject":"cs.SC","summary":"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}$,…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-25","reactions":{}}