Order 25 = 5²
0 / 2 paper-excluded 0 / 2 Lean-excluded odd candidate
Why a candidate
Order 25 = 5² is a candidate because it divides the following Theorem 6 maxima: 275, 375.
From the paper (Macaj–Siran 2010)
Lemma 18 (5-group classification): a 5-group X has
Fix(X) either Hoffman–Singleton (|X| ∣ 25,
with Proposition 3 tightening to |X| ≤ 5), a pentagon
(|X| ∣ 125), or empty (|X| ∣ 5⁶). A
non-trivial 5² subgroup needs pentagon or empty Fix; both branches
allow |X| = 25. Lemma 13 (p = 5) provides
further trace constraints. Both groups paper-allowed
— unlike the p = 7 case at order 49, Lemma 18 does not
exclude the cyclic ℤ₂₅.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(25, 1) |
ℤ₂₅ |
Cyclic; 5-group, Lem 18 allows |X|=25 in pentagon or empty Fix branch. |
allowed | open |
(25, 2) |
ℤ₅ × ℤ₅ |
Elementary abelian; 5-group, Lem 18 allows. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.