{"id":"arxiv/2606.26141","url":"https://arxiv.org/abs/2606.26141","tags":["math.HO","math.GR"],"score":0,"title":"Classifying the Groups of Order $p^3$ in Lean","domain":"math.HO","source":"arxiv","authors":["Li Xiang"],"reviews":0,"subject":"math.HO","summary":"This note discusses our formalisation in Lean 4 of the classification of groups of order $p^3$ for a prime number $p$, using mathlib4. We present the five isomorphism classes and give a detailed account of the formalisation, with particular emphasis on the non-abelian case, which requiring the most substantial formal development. For odd~$p$, the non-abelian groups are the Heisenberg group $\\Heis(\\Z/p\\Z)$ and the semidirect product $\\Z/p^2\\Z\\rtimes\\Z/p\\Z$; for $p=2$, they are $D_4$ and $Q_8$. We describe the construction of these concrete groups, the structural lemmas about centers,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-06-20","reactions":{}}