Theorem 1.3 — a regular $M_{23}$ -extension of $\mathbb{Q}(t)$

Open

MathieuM23.regular_m23_extension_ratfunc

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

inverse-galois-problemmathieu-groupnumber-theory

There exists a finite Galois extension $L/\mathbb{Q}(t)$ that is regular over $\mathbb{Q}$ (contains no nontrivial algebraic extension of $\mathbb{Q}$ ) and has Galois group isomorphic to $M_{23}$ :

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

By Hilbert's irreducibility theorem this implies Theorem 1.1, and in fact gives infinitely many $M_{23}$ -extensions of $\mathbb{Q}$ .

Formalization Note $\mathbb{Q}(t)$ is the field of rational functions over $\mathbb{Q}$ . Regularity is the predicate from the definition file.

Preamble

import Definitions.Def_MathieuM23_Group
import Definitions.Def_MathieuM23_Regular

Formal statement

namespace MathieuM23

theorem regular_m23_extension_ratfunc :
    ∃ (L : Type) (_ : Field L) (_ : Algebra (RatFunc ℚ) L),
      FiniteDimensional (RatFunc ℚ) L ∧ IsGalois (RatFunc ℚ) L ∧ IsRegularOverRatFunc L ∧
        Nonempty ((L ≃ₐ[RatFunc ℚ] L) ≃* 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. 2, Theorem 1.3 (with the definition of regular in §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. There exist a type $L$ (lowest universe), a field structure on $L$ and an algebra structure $\iota:\mathbb{Q}(t)\to L$ over the rational function field $\mathbb{Q}(t)$ in one variable, such that all four of the following hold:

$L$ is finite-dimensional over $\mathbb{Q}(t)$ ;
$L/\mathbb{Q}(t)$ is Galois;
$L$ is regular: every $x\in L$ that is a root of a nonzero polynomial with rational coefficients (coefficients mapped into $L$ via $\mathbb{Q}\subset\mathbb{Q}(t)\xrightarrow{\iota}L$ ) equals the image of some rational number;
there is an abstract group isomorphism between the group of field automorphisms of $L$ fixing $\mathbb{Q}(t)$ pointwise and $M_{23}=\langle g_1,g_2\rangle\le\mathrm{Sym}(\{0,\dots,22\})$ .

No hypotheses. Item 3 rules out, for example, $L=K(t)$ for a number field $K\ne\mathbb{Q}$ .

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.3 — a regular M23M_{23}M23​-extension of Q(t)\mathbb{Q}(t)Q(t)

Theorem 1.3 — a regular $M_{23}$ -extension of $\mathbb{Q}(t)$