Classifying the groups of order $p q$ in Lean

TL;DR

This paper presents a formalization in Lean of the classification of groups of order pq, including key results on internal product structures, enhancing the reliability of algebraic classifications through computer proof verification.

Contribution

It provides the first formal proof in Lean of the classification of groups of order pq, including characterizations of internal direct and semidirect products.

Findings

Successful formalization of group classification in Lean

Verification of characterizations of internal and semidirect products

Enhanced confidence in algebraic classifications through computer proof

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.