Order 125 = 5³
0 / 5 paper-excluded 0 / 5 Lean-excluded odd candidate
Why a candidate
Order 125 = 5³ is a candidate because it divides the following Theorem 6 maxima: 375.
From the paper (Macaj–Siran 2010)
Lemma 18 / Theorem 5 (5-group classification): a 5-group of order
125 has Fix(X) either a pentagon
(|X| ∣ 125 achieved with equality) or empty
(|X| ∣ 5⁶); the Hoffman–Singleton branch is excluded
here (Proposition 3 caps it at |X| ≤ 5). Propositions
4–5 add structural constraints but do not single out any of the 5
isomorphism types. All 5 groups paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(125, 1) | ℤ₁₂₅ | Cyclic. | allowed | open |
(125, 2) | ℤ₂₅ × ℤ₅ | Abelian, rank 2. | allowed | open |
(125, 3) | (non-abelian) | Heisenberg (exponent 5). | allowed | open |
(125, 4) | (non-abelian) | Exponent 25. | allowed | open |
(125, 5) | (ℤ₅)³ | Elementary abelian. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.