Order 11 = 11
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 11 = 11 is a candidate because it divides the following Theorem 6 maxima: 275.
From the paper (Macaj–Siran 2010)
MP 2001 Lemma 3 case (4) for p = 11 forces
Fix(ℤ₁₁) to be a pentagon (= Lemma 4 case 4 / Lemma 16
case 4). Lemma 19 case (3) further forces the 11-Sylow to be
cyclic: X ≅ ℤ₁₁, no ℤ₁₁². No direct
exclusion at order 11 — the single group ℤ₁₁ is
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(11, 1) |
ℤ₁₁ |
Cyclic; Fix(ℤ₁₁) = pentagon (Lem 3(4)); 11-Sylow forced cyclic (Lem 19(3)). |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.