← All papers

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

Li Xiang

math.HO Jun 20, 2026 · v1 math.GR

formalization mathlib algebra

Read PDF arXiv abstract Code

TL;DR

Formalizes in Lean 4 with Mathlib the classification of groups of order p^3 into five isomorphism classes.

Abstract

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, commutators, and exponents, and the explicit isomorphism constructions that classify an arbitrary non-abelian $p^3$-group.

Problem

The classification of groups of order p^3 is a classical result in finite group theory, but had not been completely formalized in any proof assistant.

Approach

The author constructs all five canonical groups (three abelian, two non-abelian) as Lean 4 structures and builds explicit isomorphisms showing any group of order p^3 falls into one of these classes. The Heisenberg group and semidirect product Z/p^2Z rtimes Z/pZ are defined with custom multiplication, and structural lemmas on centers, commutators, and exponents drive the classification.

Results

First complete formalization of the p^3 classification in any proof assistant: approximately 3,000 lines of Lean 4 code across six files, depending on Mathlib for Sylow theory and the structure theorem for finite abelian groups.

File	Content
P3Group/Defs.lean	Concrete models and P3Classification type
P3Group/Structural.lean	Center, quotient, commutator, nilpotency lemmas
P3Group/AbelianCase.lean	Abelian classification via structure theorem
P3Group/NonAbelianCase.lean	Non-abelian classification
P3Group/Classification.lean	Main theorem and pairwise non-isomorphism
P3Group.lean	Top-level import file

Project file structure

Papers With

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