§3 — $M_{23}$ has 17 conjugacy classes

Proved

MathieuM23.m23_card_conjClasses

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

group-theorymathieu-group

The group $M_{23}$ has exactly $17$ conjugacy classes:

1,\ 2,\ 3,\ 4,\ 5,\ 6,\ 7A,\ 7B,\ 8,\ 11A,\ 11B,\ 14A,\ 14B,\ 15A,\ 15B,\ 23A,\ 23B.

Formalization Note Only the number of classes is formalized, not the labelling.

Preamble

import Definitions.Def_MathieuM23_Group

Formal statement

namespace MathieuM23

theorem m23_card_conjClasses : Nat.card (ConjClasses M23) = 17 := 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. 4, §3 (list

1,2,3,4,5,6,7A,7B,8,11A,11B,14A,14B,15A,15B,23A,23B

)

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. The set of conjugacy classes of the group $M_{23}=\langle g_1,g_2\rangle$ has exactly $17$ elements. Two elements are in the same class when they are conjugate by an element of $M_{23}$ itself, not of the full permutation group. Cardinality is counted as a natural number. No hypotheses. Class names, element orders and the list of classes are not part of the statement.

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

§3 — M23M_{23}M23​ has 17 conjugacy classes

§3 — $M_{23}$ has 17 conjugacy classes