The Mathieu group $M_{23}$ as a subgroup of $S_{23}$

Definition

MathieuM23_Group

by Lucas · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-theorymathieu-grouppermutation-groups

Let $S_{23}$ be the symmetric group on $23$ points, acting on the left. Following §3 of the source, define the permutations

g_1=(1,11)(2,23)(3,8)(4,16)(5,21)(7,20)(15,19)(18,22),

g_2=(1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12),

g_3=(1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23).

The Mathieu group is $M_{23}:=\langle g_1,g_2\rangle\le S_{23}$ . For $g\in S_{23}$ , the $M_{23}$ -conjugacy class of $g$ is $\{kgk^{-1}: k\in M_{23}\}$ .

These are the basic objects of every statement in the mission: the group $M_{23}$ , its explicit generators, and the third element $g_3$ of the triple $(g_1,g_2,g_3)$ used to build the $M_{23}$ -cover.

Formalization Note The points $1,\dots,23$ are encoded as Fin 23 via $k\mapsto k-1$ . The helper labelPerm takes the cycles in the paper's labels and performs this shift. Permutations compose as functions, matching the paper's left action.

Definition code

import Mathlib

/-!
# The Mathieu group `M₂₃` as a permutation group (Huang–Jackson–Lee–Poonen–Pries–Zhang, §3)

Points `1, …, 23` of the paper are encoded as elements of `Fin 23` by `k ↦ k - 1`;
`MathieuM23.labelPerm` performs this shift, so the cycles below are copied verbatim from the paper.
Permutations act on the left: `(σ * τ) x = σ (τ x)`, matching the paper's footnote 3.
-/

namespace MathieuM23

/-- The permutation of `Fin 23` given by a list of disjoint cycles written with the paper's
labels `1, …, 23` (label `k` is the element `k - 1 : Fin 23`). -/
def labelPerm (cycles : List (List ℕ)) : Equiv.Perm (Fin 23) :=
  (cycles.map fun c => (c.map fun k => (Fin.ofNat 23 (k - 1))).formPerm).prod

/-- `g₁ = (1,11)(2,23)(3,8)(4,16)(5,21)(7,20)(15,19)(18,22)`. -/
def g₁ : Equiv.Perm (Fin 23) :=
  labelPerm [[1, 11], [2, 23], [3, 8], [4, 16], [5, 21], [7, 20], [15, 19], [18, 22]]

/-- `g₂ = (1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12)`. -/
def g₂ : Equiv.Perm (Fin 23) :=
  labelPerm [[1, 2, 11, 10, 16, 9, 6, 3, 23, 19, 20, 14, 21, 17, 4, 8, 22, 5, 18, 15, 13, 7, 12]]

/-- `g₃ = (1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23)`. -/
def g₃ : Equiv.Perm (Fin 23) :=
  labelPerm [[1, 2, 3, 4, 10, 11, 12, 7, 19, 18, 8, 6, 9, 16, 17, 21, 22, 5, 14, 20, 13, 15, 23]]

/-- The Mathieu group `M₂₃`, the subgroup of `S₂₃` generated by `g₁` and `g₂`. -/
def M23 : Subgroup (Equiv.Perm (Fin 23)) :=
  Subgroup.closure {g₁, g₂}

/-- The conjugacy class in `M₂₃` of a permutation `g`: all `k g k⁻¹` with `k ∈ M₂₃`. -/
def classIn (g : Equiv.Perm (Fin 23)) : Set (Equiv.Perm (Fin 23)) :=
  {h | ∃ k ∈ M23, h = k * g * k⁻¹}

end MathieuM23

Source

X. Huang, B. Jackson, K.-H. Lee, B. Poonen, R. Pries, S. Zhang, *The Mathieu group M23 is a Galois group over Q*, arXiv:2608.08538v1 (2026), https://arxiv.org/abs/2608.08538, p. 4–5, §3 (generators

g_1,g_2

and the permutation

g_3

; footnote 3 on the left action)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Disclosure — NON-BLIND read-back. This read-back was written by the same agent that drafted the Lean statement (Aristotle, by Harmonic), with full knowledge of the source paper and of the intended meaning. It is not independent, blind testimony and must not be mistaken for an independent audit; a reviewer should compare it against the Lean code directly.

This file introduces four objects inside the namespace MathieuM23.

Label conversion. For a list of lists of natural numbers $[c_1,\dots,c_r]$ , the permutation of $\{0,\dots,22\}$ is the product $\pi_{c_1}\pi_{c_2}\cdots\pi_{c_r}$ (composition of functions, rightmost applied first). Here $\pi_c$ is the cyclic permutation of the list obtained from $c=[k_1,\dots,k_m]$ by replacing each $k_j$ by $(k_j-1)\bmod 23$ . That permutation sends the $j$ -th entry to the $(j+1)$ -st, the last entry to the first, and fixes everything else. If a list has repeated entries, or entries $0$ or $>23$ , the result is still some permutation, but not a cycle in the usual sense. All lists used below have distinct entries in $\{1,\dots,23\}$ and are pairwise disjoint.
The three permutations $g_1,g_2,g_3$ of $\{0,\dots,22\}$ are obtained this way from the cycle lists $[[1,11],[2,23],[3,8],[4,16],[5,21],[7,20],[15,19],[18,22]]$ , $[[1,2,11,10,16,9,6,3,23,19,20,14,21,17,4,8,22,5,18,15,13,7,12]]$ and $[[1,2,3,4,10,11,12,7,19,18,8,6,9,16,17,21,22,5,14,20,13,15,23]]$ respectively. So in labels $1..23$ , $g_1$ is a product of $8$ disjoint transpositions and $g_2$ , $g_3$ are the displayed $23$ -cycles.
The subgroup $M_{23}$ is the subgroup of the full permutation group of $\{0,\dots,22\}$ generated by the two elements $g_1$ and $g_2$ alone. $g_3$ is not a generator. Nothing in the definition asserts its order, simplicity, or that $g_3\in M_{23}$ .
Conjugacy class in $M_{23}$ . For any permutation $g$ (not required to lie in $M_{23}$ ), $\mathrm{cl}(g)=\{h : \exists k\in M_{23},\ h=kgk^{-1}\}$ , with the product read as composition.

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Mathieu group M23M_{23}M23​ as a subgroup of S23S_{23}S23​

The Mathieu group $M_{23}$ as a subgroup of $S_{23}$