Order 27 = 3³
0 / 5 paper-excluded 0 / 5 Lean-excluded odd candidate
Why a candidate
Order 27 = 3³ is a candidate because it divides the following Theorem 6 maxima: 135.
From the paper (Macaj–Siran 2010)
Lemma 17 (3-group classification): a 3-group of order 27 has
Fix(X) the Petersen graph (Petersen branch's bound
|X| ∣ 27 is met with equality; the singleton branch
|X| ∣ 81 also allows 27). Theorem 4 caps 3-group
Aut(Γ)-subgroups at order 27. The paper does not single out any of
the 5 isomorphism types as excluded. All 5 groups
paper-allowed.
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(27, 1) | ℤ₂₇ | Cyclic. | allowed | open |
(27, 2) | ℤ₉ × ℤ₃ | Abelian, rank 2. | allowed | open |
(27, 3) | Heisenberg | Non-abelian, exponent 3. | allowed | open |
(27, 4) | ℤ₉ ⋊ ℤ₃ | Non-abelian, exponent 9. | allowed | open |
(27, 5) | (ℤ₃)³ | Elementary abelian. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.