Order 15 = 3 · 5
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 15 = 3 · 5 is a candidate because it divides the following Theorem 6 maxima: 135, 375.
From the paper (Macaj–Siran 2010)
Lemma 15 row pq = 15 gives a₀, a₁
constraints; no row is starred, so order-15 elements may exist.
Per-prime: Lemma 17 / MP 2001 Lem 3(2/5) for the 3-part gives
Fix(ℤ₃) ∈ {singleton, Petersen}; Lemma 18 /
Lem 3(1/4/6) for the 5-part gives
Fix(ℤ₅) ∈ {empty, pentagon, HS}. The single
cyclic group ℤ₁₅ is paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(15, 1) |
ℤ₁₅ |
Cyclic (3 ∤ 5 − 1, so only the abelian group exists). |
allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.