Example 1.2 — an explicit $M_{23}$ -polynomial unramified outside $\{2,3,23\}$

Open

MathieuM23.example_1_2

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

inverse-galois-problemmathieu-groupnumber-theory

Let $f=f_{1.2}\in\mathbb{Q}[x]$ be the degree-23 polynomial of Example 1.2 and let $K$ be a splitting field of $f$ over $\mathbb{Q}$ . Then:

$K/\mathbb{Q}$ is Galois;
$\mathrm{Gal}(K/\mathbb{Q})\cong M_{23}$ ;
$K$ is unramified outside $\{2,3,23\}$ : every prime $p$ dividing the discriminant $d_K$ belongs to $\{2,3,23\}$ .

\mathrm{Gal}(K/\mathbb{Q})\cong M_{23},\qquad p\mid d_K\ \Rightarrow\ p\in\{2,3,23\}.

A formal proof gives an explicit, independently checkable witness of Theorem 1.1.

Formalization Note The statement is made for every number field $K$ that is a splitting field of $f$ , which does not lose generality because splitting fields are unique up to isomorphism. "Unramified outside $S$ " is encoded through the absolute discriminant, which is equivalent by Dedekind's discriminant theorem.

Preamble

import Definitions.Def_MathieuM23_Group
import Definitions.Def_MathieuM23_Polynomials

Formal statement

namespace MathieuM23

theorem example_1_2 (K : Type) [Field K] [NumberField K]
    [Polynomial.IsSplittingField ℚ K fEx12] :
    IsGalois ℚ K ∧ Nonempty ((K ≃ₐ[ℚ] K) ≃* M23) ∧
      ∀ p : ℕ, p.Prime → (p : ℤ) ∣ NumberField.discr K → p = 2 ∨ p = 3 ∨ p = 23 := 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–2, Example 1.2

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. Let $K$ be any type in the lowest universe carrying a field structure that is a number field (characteristic $0$ and finite-dimensional over $\mathbb{Q}$ , with its canonical $\mathbb{Q}$ -algebra structure). Assume $K$ is a splitting field over $\mathbb{Q}$ of the explicit degree-23 polynomial $f_{1.2}$ . That is, $f_{1.2}$ splits into linear factors in $K$ and $K$ is generated over $\mathbb{Q}$ by its roots. Then all of the following hold:

$K/\mathbb{Q}$ is a Galois extension;
there is a group isomorphism $\mathrm{Aut}_{\mathbb{Q}}(K)\cong M_{23}$ , where $M_{23}=\langle g_1,g_2\rangle$ is the explicit permutation group on $\{0,\dots,22\}$ (abstract group isomorphism only);
for every prime natural number $p$ , if $p$ divides (as an integer) the absolute discriminant $d_K\in\mathbb{Z}$ of the number field $K$ , then $p=2$ , $p=3$ or $p=23$ .

Here

f_{1.2}=x^{23}-184x^{21}-1150x^{20}+\dots+19169943578802x-3150159884154,

with the full coefficient list in the polynomial definition file. Ramification is not mentioned directly; only the discriminant condition appears. The hypotheses are satisfiable: a splitting field exists and is a number field.

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

Example 1.2 — an explicit M23M_{23}M23​-polynomial unramified outside {2,3,23}\{2,3,23\}{2,3,23}

Example 1.2 — an explicit $M_{23}$ -polynomial unramified outside $\{2,3,23\}$