Classifying the Groups of Order $p^3$ in Lean

Li Xiang

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 g…