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