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

Li Xiang

Reviewed by Pith at T0; open to challenge.

T0 means a machine referee read the full paper against a public rubric. The mark states how deep the mechanical check went, never who wrote it. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

Every group of order p^3 is isomorphic to one of five standard groups.

2026-06-26 11:05 UTC pith:GDYT3SUJ

load-bearing objection A straightforward Lean formalization of the classical p^3 group classification that adds to mathlib but introduces no new mathematics.

arxiv 2606.26141 v1 pith:GDYT3SUJ submitted 2026-06-20 math.HO math.GR

Classifying the Groups of Order p³ in Lean

Li Xiang This is my paper

classification math.HO math.GR

keywords p-groupsgroup classificationisomorphism classesnon-abelian groupsHeisenberg groupsemidirect productdihedral groupquaternion group

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that groups of order p cubed for prime p fall into exactly five isomorphism classes. It supplies concrete models for the three abelian cases as direct products of cyclic groups and for the non-abelian cases as the Heisenberg group together with a semidirect product when p is odd, or the dihedral and quaternion groups when p equals 2. Structural facts about centers, commutators and exponents are used to separate the classes, after which explicit maps are built to show that an arbitrary group of this order matches one of the five. A sympathetic reader would care because the result supplies a complete, step-by-step identification procedure that removes any possibility of overlooked cases in the classical listing.

Core claim

The classification asserts that there are five isomorphism types of groups of order p^3. The abelian ones are the cyclic group of order p^3, the direct product of cyclic groups of orders p^2 and p, and the direct product of three copies of the cyclic group of order p. For odd p the non-abelian groups are the Heisenberg group over the integers modulo p, which has exponent p, and the semidirect product of the cyclic group of order p^2 by the cyclic group of order p. When p equals 2 the non-abelian groups are the dihedral group of order 8 and the quaternion group of order 8. The development constructs each of these groups and supplies the explicit isomorphisms that classify every non-abelian gr

What carries the argument

Explicit isomorphism constructions that send an arbitrary non-abelian group of order p^3 to one of the two standard models, using lemmas on the center, the commutator subgroup, and the exponent.

Load-bearing premise

The definitions of groups, semidirect products, centers, commutators, and isomorphisms match the standard mathematical notions used in the classical proof.

What would settle it

A concrete group of order p cubed whose structure cannot be matched to any of the five listed models by the supplied isomorphisms would falsify the classification.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

Any group of order p^3 belongs to one of the five classes and can be identified by computing its center size, commutator size, and exponent.
The two non-abelian classes for odd p are separated exactly by whether the exponent equals p or p squared.
Every non-abelian group of order p^3 has center and derived subgroup both of order p.
The three abelian classes correspond to the three possible partitions of the integer 3.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same pattern of explicit isomorphism maps could be used to classify groups of order p^4.
Having the small cases settled allows mechanical verification of further statements about representations or automorphisms of these groups.
The distinction between the Heisenberg group and the semidirect product supplies a model case for studying nilpotent groups of class two.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

A straightforward Lean formalization of the classical p^3 group classification that adds to mathlib but introduces no new mathematics.

read the letter

This paper records a Lean 4 formalization, via mathlib4, of the five isomorphism classes of groups of order p^3. The main contribution is the explicit construction of the non-abelian examples (Heisenberg group and semidirect product for odd p; D4 and Q8 for p=2) together with the structural lemmas on centers, commutators, and the explicit isomorphisms that finish the classification.

The work is competent on its own terms. It follows the standard textbook proof, builds the groups from the library primitives, and verifies the necessary properties without apparent shortcuts. That is useful for anyone who wants the result already checked inside mathlib rather than having to redo the lemmas themselves.

The obvious limitation is that the theorem itself has been known since the 19th century and the paper makes no claim to new mathematics. The value is therefore entirely in the formalization effort and the integration with existing library definitions. Because the abstract gives no commit hash or proof statistics, a referee would still want to inspect the actual code to confirm the development is complete and not merely sketched.

The paper is aimed at the small community that maintains and uses mathlib4 for group theory. A reader already working in that setting will find the explicit constructions and the handling of the p=2 case worth looking at. Outside that circle the paper adds little.

I would send it to peer review at a venue that publishes formalizations; the work is honest and the central claim is mechanically verified once the code is examined. It does not need to be desk-rejected.

Referee Report

0 major / 2 minor

Summary. The paper claims to have formalized in Lean 4 using mathlib4 the classification of groups of order p^3 for prime p into five isomorphism classes. It presents the three abelian groups (Z/p^3Z, Z/p^2Z × Z/pZ, Z/pZ × Z/pZ × Z/pZ) and the two non-abelian ones (Heisenberg group Heis(Z/pZ) and Z/p^2Z ⋊ Z/pZ for odd p; D4 and Q8 for p=2), along with structural lemmas on centers, commutators, and exponents, and explicit isomorphism constructions to classify arbitrary non-abelian p^3-groups.

Significance. This is a replication of a standard theorem rather than a novel result, but the machine-checked formalization and detailed account of the proof structure (particularly the non-abelian cases via semidirect products) provide a useful reference implementation within the Lean ecosystem. It demonstrates the applicability of mathlib4's Group, SemidirectProduct, center, commutator, and Iso primitives to a complete classification and can serve as an educational blueprint for similar formalizations of finite group theory results.

minor comments (2)

The manuscript does not include a link to the code repository, commit hash, or Lean file names, which would improve reproducibility and allow readers to inspect the proof structure directly.
The abstract and introduction could more explicitly state the three abelian isomorphism classes alongside the non-abelian ones for completeness.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the formalization and for recommending minor revision. No major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; formalization of classical result via external library

full rationale

The paper is a Lean 4 formalization (via mathlib4) of the standard classification of groups of order p^3 into five isomorphism classes. It constructs the groups (Heisenberg, semidirect products, D4, Q8), proves structural properties of centers/commutators/exponents, and exhibits explicit isomorphisms. All load-bearing definitions and lemmas are supplied by the external mathlib4 library rather than by self-referential equations or author-specific ansatzes. No fitted parameters, no predictions that reduce to inputs by construction, and no uniqueness theorems imported from the authors' prior work. The sole assumption—that mathlib4's Group/SemidirectProduct/center/commutator/Iso coincide with classical notions—is an external verification condition, not an internal circular reduction. The derivation chain is therefore self-contained against the library and the classical theorem.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper introduces no new free parameters, invented entities, or ad-hoc axioms; it formalizes existing group-theoretic structures using standard definitions from mathlib4.

axioms (1)

standard math Standard axioms of group theory and the definitions of semidirect product, center, commutator, and isomorphism as provided by mathlib4.
The formalization is built directly on these library definitions.

pith-pipeline@v0.9.1-grok · 5667 in / 1176 out tokens · 24569 ms · 2026-06-26T11:05:02.649370+00:00 · methodology

0 comments

read the original 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.

discussion (0)

Reference graph

Works this paper leans on

5 extracted references · 2 canonical work pages

[1]

Gonthier et al.,A machine-checked proof of the odd order theorem, ITP 2013, LNCS 7998, Springer, 2013, 163–179

G. Gonthier et al.,A machine-checked proof of the odd order theorem, ITP 2013, LNCS 7998, Springer, 2013, 163–179

2013
[2]

9th ACM SIGPLAN CPP, ACM, 2020, 367–381,https://github.com/leanprover-community/mathlib4

Themathlibcommunity,The Lean mathematical library, Proc. 9th ACM SIGPLAN CPP, ACM, 2020, 367–381,https://github.com/leanprover-community/mathlib4

2020
[3]

Harper and P

S. Harper and P. Wu,Classifying the groups of orderpqin Lean, preprint, arXiv:2501.09769, 2025

work page arXiv 2025
[4]

Automated

L. de Moura, S. Kong, J. Avigad, F. van Doorn and J. von Raumer,The Lean theorem prover (system description), CADE 25, LNCS 9195, Springer, 2015, 378–388,https://doi. org/10.1007/978-3-319-21401-6_26. 12

work page doi:10.1007/978-3-319-21401-6_26 2015
[5]

com/lixiang90/p3group

Li Xiang,P3Group: Classification of groups of orderp 3 in Lean, 2026,https://github. com/lixiang90/p3group. 13

2026

[1] [1]

Gonthier et al.,A machine-checked proof of the odd order theorem, ITP 2013, LNCS 7998, Springer, 2013, 163–179

G. Gonthier et al.,A machine-checked proof of the odd order theorem, ITP 2013, LNCS 7998, Springer, 2013, 163–179

2013

[2] [2]

9th ACM SIGPLAN CPP, ACM, 2020, 367–381,https://github.com/leanprover-community/mathlib4

Themathlibcommunity,The Lean mathematical library, Proc. 9th ACM SIGPLAN CPP, ACM, 2020, 367–381,https://github.com/leanprover-community/mathlib4

2020

[3] [3]

Harper and P

S. Harper and P. Wu,Classifying the groups of orderpqin Lean, preprint, arXiv:2501.09769, 2025

work page arXiv 2025

[4] [4]

Automated

L. de Moura, S. Kong, J. Avigad, F. van Doorn and J. von Raumer,The Lean theorem prover (system description), CADE 25, LNCS 9195, Springer, 2015, 378–388,https://doi. org/10.1007/978-3-319-21401-6_26. 12

work page doi:10.1007/978-3-319-21401-6_26 2015

[5] [5]

com/lixiang90/p3group

Li Xiang,P3Group: Classification of groups of orderp 3 in Lean, 2026,https://github. com/lixiang90/p3group. 13

2026