Corollary 3.6 (group-theoretic step) — $M_{23}$ is not normal in any larger subgroup of $S_{23}$

Proved

MathieuM23.m23_self_normalizing

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

group-theorymathieu-grouppermutation-groups

If $H$ is a subgroup of $S_{23}$ with $M_{23}\le H$ and $M_{23}\trianglelefteq H$ , then $H=M_{23}$ . Equivalently, $M_{23}$ is self-normalizing in $S_{23}$ :

N_{S_{23}}(M_{23})=M_{23}.

This is the group-theoretic input that upgrades $G_{\mathrm{geom}}=M_{23}$ to $G_{\mathrm{arith}}=M_{23}$ in Corollary 3.6.

Preamble

import Definitions.Def_MathieuM23_Group

Formal statement

namespace MathieuM23

theorem m23_self_normalizing (H : Subgroup (Equiv.Perm (Fin 23))) (hle : M23 ≤ H)
    (hnormal : (M23.subgroupOf H).Normal) : H = 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. 7, proof of Corollary 3.6 ("

M_{23}

is not normal in any larger subgroup of

S_{23}

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 $H$ be any subgroup of the permutation group of $\{0,\dots,22\}$ . Assume (i) $M_{23}\subseteq H$ and (ii) $M_{23}$ , viewed as a subgroup of the group $H$ , is normal in $H$ . Then $H=M_{23}$ . Both hypotheses are satisfiable, e.g. by $H=M_{23}$ . Here $M_{23}=\langle g_1,g_2\rangle$ .

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

Corollary 3.6 (group-theoretic step) — M23M_{23}M23​ is not normal in any larger subgroup of S23S_{23}S23​

Corollary 3.6 (group-theoretic step) — $M_{23}$ is not normal in any larger subgroup of $S_{23}$