Theorem 1.1 — $M_{23}$ is a Galois group over $\mathbb{Q}$

Open

MathieuM23.m23_galois_group_over_rat

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

inverse-galois-problemmathieu-groupnumber-theory

Let $M_{23}\le S_{23}$ be the Mathieu group, generated by the permutations $g_1,g_2$ of the source. Then there exists a finite Galois extension $K/\mathbb{Q}$ whose Galois group is isomorphic to $M_{23}$ :

\exists\,K/\mathbb{Q}\ \text{finite Galois}:\qquad \mathrm{Gal}(K/\mathbb{Q})\cong M_{23}.

This is the last sporadic simple group to be realized as a Galois group over $\mathbb{Q}$ .

Formalization Note $K$ ranges over fields in the lowest universe with a $\mathbb{Q}$ -algebra structure. The Galois group is the group of $\mathbb{Q}$ -algebra automorphisms of $K$ , and the conclusion is the existence of a group isomorphism with the subgroup $M_{23}$ .

Preamble

import Definitions.Def_MathieuM23_Group

Formal statement

namespace MathieuM23

theorem m23_galois_group_over_rat :
    ∃ (K : Type) (_ : Field K) (_ : Algebra ℚ K),
      FiniteDimensional ℚ K ∧ IsGalois ℚ K ∧ Nonempty ((K ≃ₐ[ℚ] K) ≃* M23) := by sorry

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. 1, Theorem 1.1

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.

Statement. There exist a type $K$ (in the lowest universe), a field structure on $K$ and a $\mathbb{Q}$ -algebra structure on $K$ such that all three of the following hold:

$K$ is finite-dimensional as a vector space over $\mathbb{Q}$ ;
$K/\mathbb{Q}$ is a Galois extension (normal and separable);
there is a group isomorphism between the group $\mathrm{Aut}_{\mathbb{Q}}(K)$ of field automorphisms of $K$ fixing $\mathbb{Q}$ (under composition) and $M_{23}$ .

Here $M_{23}$ is the subgroup of the permutation group of $\{0,\dots,22\}$ generated by the two explicit permutations $g_1$ (a product of 8 transpositions) and $g_2$ (a 23-cycle) from the group definition file. The isomorphism is only required to be an abstract group isomorphism; no action on roots or on $\{0,\dots,22\}$ is involved. The statement has no hypotheses. Since $M_{23}$ has more than one element, $K=\mathbb{Q}$ would not witness it.

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

Theorem 1.1 — M23M_{23}M23​ is a Galois group over Q\mathbb{Q}Q

Theorem 1.1 — $M_{23}$ is a Galois group over $\mathbb{Q}$