Order 5 = 5
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 5 = 5 is a candidate because it divides the following Theorem 6 maxima: 35, 135, 275, 375.
From the paper (Macaj–Siran 2010)
MP 2001 Lemma 3 cases (1) / (4) / (6) for p = 5 give
Fix(ℤ₅) ∈ {empty, pentagon, HS} (= Lemma 4 cases 1, 4, 6
/ Lemma 16 same). Lemma 18 then bounds any 5-group:
|X| ∣ 25 (HS-Fix), |X| ∣ 125 (pentagon-Fix),
or |X| ∣ 5⁶ (empty-Fix). No direct exclusion at
order 5 — the single group ℤ₅ is
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(5, 1) |
ℤ₅ |
Cyclic; Fix(ℤ₅) ∈ {empty, pentagon, HS} (Lem 3(1/4/6)). |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.