REVIEW 4 minor 10 references
Classifying the groups of order $p q$ in Lean
T0 review · 0 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash
Pith's one-line read The paper establishes in the Lean theorem prover a machine-checked classification of all groups of order $p q$ for prime numbers $p$ and $q$.
desk verdict A clean, credible formalization note: the math is textbook, the reusable Lean lemmas are the real contribution, and the only real caveat is reproducibility hygiene (no pinned mathlib commit). read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The machine-checked proof is carried by the internal semidirect product characterisation `mulEquivSemidirectProduct`, which turns the subgroup conditions $N \sqcap H = \bot$ and $N \sqcup H = \top$ into an explicit isomorphism $G \cong N \rtimes_\varphi H$ with $\varphi$ the conjugation action restricted to $H$, together with its direct-product counterpart `mulEquivProd`. To give a concrete target for the classification, the paper defines `MulZMod n`, the multiplicative version of the additive group `ZMod n`, as a cyclic group of order $n$, and states the noncyclic groups of order $p q$ as `MulZMod q ⋊[φ] MulZMod p`. A key mathematical input is that $\operatorname{Aut}(C_p) \cong C_{p-1}$, obtained by identifying the automorphism group of `ZMod p` with the unit group of the finite integral domain `ZMod p` and using the cyclicity of that unit group.
What would settle it
Open the linked Lean repository and check that the five declarations in Figure 1 are accepted by the Lean kernel with no `axiom`, `sorry`, or `admit` among their dependencies; if any such gap appears, or if the statements differ from Figure 1, the claim of a machine-checked classification is not established.
Extended reading notes
Core claim
The central claim is that a finite group $G$ with $|G| = p q$, where $p$ and $q$ are prime, is cyclic unless $p = q$ or one of $p, q$ divides one less than the other. In the noncyclic case $G$ is isomorphic either to $C_p \times C_p$ (when $p = q$) or to the semidirect product $C_q \rtimes C_p$ (when $p < q$ and $p \mid q-1$), and any two such noncyclic groups are isomorphic. The paper packages this as five explicit Lean theorems, including the iff statement `exists_card_eq_prime_mul_prime_and_not_isCyclic_iff` and the uniqueness statement `nonempty_mulEquiv_of_card_eq_prime_mul_prime_of_not_isCyclic`. It also formalises Lemma 2.2: if subgroups $N, H \le G$ satisfy $HN = G$ and $H \cap N = 1$, with $N$ normal, then $G$ is isomorphic to the semidirect product $N \rtimes_\varphi H$, and if both subgroups are normal then $G \cong H \times N$.
Load-bearing premise
The formal proof inherits the correctness of the existing library it imports, especially the facts that the unit group of a finite integral domain is cyclic and that the unit group of `ZMod p` has size $p-1$, along with the library's encoding of groups, subgroups, and semidirect products.
Editorial extensions
If this is right
- The formal iff theorem gives a complete existence criterion: a noncyclic group of order $p q$ exists exactly when $p = q$, $p \mid q - 1$, or $q \mid p - 1$.
- Because the statements are uniform in $p$ and $q$, the classification of groups of order $p^2$ is included as the special case $p = q$.
- The reusable `mulEquivSemidirectProduct` and `mulEquivProd` lemmas provide a standard route for proving that a group with two complementary subgroups is a semidirect or direct product, which is the central structural step of the proof.
- The uniqueness theorem asserts that any two noncyclic groups of order $p q$ are isomorphic, so mathematicians can speak of 'the' noncyclic group of order $p q$ whenever one exists.
- The code, once incorporated into the library, gives later formalisation projects a certified classification statement to cite instead of reproving the classification.
Reading between the lines
- The same internal semidirect product characterisation is a natural building block for the next classifications, such as groups of order $p^3$ or $p^2 q$, where the same subgroup-complement pattern recurs.
- The decision to work with `MulZMod` as a concrete multiplicative representative of $C_n$ suggests a template for stating future classification theorems as explicit isomorphisms to named models, rather than only as existential statements.
- If the classification is absorbed into the library, then any later formal proof involving groups of order $p q$ can rely on it; the main fragility would be that a future refactor of the unit-group cyclicity theorems would force rechecking the proof's dependency chain.
Formalized claims in Lean
-
Claim #1: The central claim is that a finite group $G$ with $|G| = p q$, where $p$ and $q$ are prime, is cyclic unless $p = q$ or one of $p, q$ divides one less than the other. In the noncyclic case $G$ is isomorphic either to $C_p \times C_p$ (when $p = q$) or to the semidirect product $C_q \rtimes C_p$ (when $p < q$ and $p \mid q-1$), and any two such noncyclic groups are isomorphic. The paper packages th
/-- @claim 1 The central claim is that a finite group $G$ with $|G| = p q$, where $p$ and $q$ are prime, is cyclic unless $p = q$ or one of $p, q$ divides one less than the other. In the noncyclic case $G$ is isomorphic either to $C_p \times C_p$ (when $p = q$) or to the semidirect product $C_q \rtimes C_p$ (when $p < q$ and $p \mid q-1$), and any two such noncyclic groups are isomorphic. The paper packages th -/ def central_claim : Prop :=
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper reports a Lean formalisation of the classification of groups of order p q for primes p and q, not necessarily distinct. The main formal theorems, displayed in Figure 1, express the existence and uniqueness up to isomorphism of noncyclic groups of order p q, the structure of noncyclic groups of order p^2 as C_p × C_p, and the semidirect-product description for p < q. The paper also formalises the internal characterisations of direct and semidirect products (Figure 2) and discusses implementation choices: the concrete cyclic group MulZMod, the use of Nat.card and Finite instead of Fintype, design choices in stating classification results, the semidirect-product API, and the proof that Aut(C_p) is cyclic of order p−1 via ZMod ring theory. The Lean code is available at the linked repository [8].
Significance. If the linked code compiles, this is a useful, machine-checked addition to mathlib's finite group theory coverage. The formal statements in Figure 1 appear faithful to Theorem 2.1, including the p = q case and the divisibility conditions, and the proof dependencies (Sylow theory, internal product characterisations, cyclicity of the unit group of a finite integral domain) are standard. There is no circular use of the classification being proved. The paper is also transparent about formal choices such as multiplicative ZMod representatives and the use of Nonempty isomorphism statements. The main residual concern, that the repository is unpinned and was not independently compiled, is a reproducibility caveat rather than an identified mathematical flaw; I did not recompile the code myself.
minor comments (4)
- [Section 2, paragraph after Theorem 2.1] The sentence 'a semidirect product Cq ⋊φ Cp depends on a choice of homomorphism φ : Cq → Aut(Cp)' swaps the domain and codomain; it should be φ : Cp → Aut(Cq), since Cq is the normal factor. The subsequent existence condition 'p | q−1' is consistent with the corrected direction, and the proof outline later states the correct direction, so this is a typo rather than a mathematical error.
- [Section 3, first paragraph and reference [8]] For reproducibility, please state the Lean version and a pinned mathlib commit at which the development compiles, and ideally include the output of `#print axioms` for the five main theorems. The current text says the imports can be found in the source code, but without a pinned commit the reader cannot independently reconstruct the exact environment.
- [Section 4.1] There is a typo: 'Mulplicative' should be 'Multiplicative'. Similar typographical issues ('efficient', 'sufficient') appear in Section 4.3.
- [Figure 2] The statement of `mulEquivProd` is correct, but it would be helpful for the caption to note explicitly that the direct-product characterisation is derived from the semidirect-product one via the trivial action; the prose says this, but a one-sentence reference in the caption would aid readability.
Circularity Check
No significant circularity: the Lean formalisation is derived from standard mathlib group/ring theory results, not from the classification being proved.
full rationale
The paper's central claim is that the classification of groups of order pq for primes p and q is formalised in Lean. The five theorem statements in Figure 1 are transcriptions of Theorem 2.1, and the proof outline in Section 2 uses standard ingredients: Lagrange's theorem, Sylow theory, the characterisation of internal direct and semidirect products (Lemma 2.2), and the fact that Aut(C_p) is cyclic of order p-1. The latter is proved in Section 4.5 from existing mathlib results about ZMod as a finite integral domain, namely that the unit group of a finite integral domain is cyclic and that the number of units is the Euler totient. None of these inputs is the classification of groups of order pq itself, and no parameter is fitted to the target data. The only self-references are citations to the authors' own repository [8] for the Lean code and to existing mathlib formalisations of prime-order and order-four groups; these are contextual or code-locating, not load-bearing assumptions of the proof. The residual concerns, such as the absence of a pinned mathlib commit or a displayed axiom dump, are reproducibility/verification caveats about the linked repository rather than circularity in the mathematical derivation.
Assumptions & free parameters
assumptions (2)
- standard math Existing mathlib theorems used in the proof, including Lagrange's theorem, cyclicity of units of finite integral domains, and Euler totient cardinality, are correct and apply as imported.
- domain assumption The Lean definitions of Group, Subgroup, Nat.card, and SemidirectProduct formalize the intended mathematical concepts, and the new MulZMod wrapper faithfully represents a cyclic group of order n.
Cite this review
Pith. "Pith review of Classifying the groups of order $p q$ in Lean." pith.science (2026). https://pith.science/paper/LJ6UGQJN
@misc{pith2026250109769,
author = {Pith},
title = {Pith review of: Classifying the groups of order $p q$ in Lean},
year = {2026},
howpublished = {\url{https://pith.science/paper/LJ6UGQJN}},
note = {Machine review of arXiv:2501.09769}
}
abstract
This note discusses our formalisation in Lean of the classification of the groups of order $p q$ for (not necessarily distinct) prime numbers $p$ and $q$, together with various intermediate results such as the characterisation of internal direct and semidirect products.
Figures
Figures from the paper (3 more)
Reference graph
Works this paper leans on
- [8]
-
[1]
Y. Bertot and P. Castéran, Interactive theorem proving and program development: Coq’Art: the calculus of inductive constructions , Texts Theoret. Comput. Sci. EATCS Ser., Springer-Verlag, 2004
work page 2004
-
[2]
J. Commelin, A. Topaz and the Lean community, The liquid tensor experiment , 2022, https://github. com/leanprover-community/lean-liquid
work page 2022
-
[3]
L. de Moura, S. Kong, J. A vigad, F. van Doorn and J. von Raumer, The Lean theorem prover (system description), in Automated deduction—CADE 25 , Lecture Notes in Comput. Sci., vol. 9195, Springer, 2015, 378–388. 8 SCOTT HARPER AND PEIRAN WU
work page 2015
-
[4]
Y. Dillies, B. Mehta and T. Tao, The polynomial Freiman–Ruzsa conjecture, 2023, https://github.com/ teorth/pfr
work page 2023
-
[5]
G. Gonthier, A. Asperti, J. A vigad and et al., A machine-checked proof of the odd order theorem , in Interactive theorem proving, Lecture Notes in Comput. Sci., vol. 7998, Springer, 2013, 163–179
work page 2013
-
[6]
D. Gorenstein, R. Lyons and R. Solomon, The classification of the finite simple groups , Mathematical Surveys and Monographs, vol. 40.1, American Mathematical Society, 1994
work page 1994
-
[7]
W. T. Gowers, B. Green, F. Manners and T. Tao, On a conjecture of Marton , preprint, arXiv:2311.05762
Show all 10 references
-
[9]
M. W. Liebeck, C. E. Praeger and J. Saxl, On the O’Nan-Scott theorem for finite primitive permutation groups, J. Austral. Math. Soc. Ser. A 44 (1988), 389–396
1988
-
[10]
The mathlib community, The Lean mathematical library , in Proceedings of the 9th ACM SIGPLAN Interna- tional Conference on Certified Programs and Proofs , CPP 2020, Association for Computing Machinery, 2020, 367–381. Scott Harper, School of Mathematics and Statistics, Universi...
2020
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.