Order 1 = 1
0 / 1 paper-excluded 0 / 1 Lean-excluded odd candidate
Why a candidate
Order 1 = 1 is a candidate because it divides the following Theorem 6 maxima: 35, 39, 135, 147, 171, 275, 375.
From the paper (Macaj–Siran 2010)
Order 1 is the trivial automorphism group: Γ would be an asymmetric graph. The paper does not address this case (it is implicit; not ruled out by any lemma). Paper-allowed (vacuously).
Group classification
| SmallGroup | Group | Description | Paper | Lean |
|---|---|---|---|---|
(1, 1) |
1 |
Trivial group; vacuously satisfies every paper hypothesis. | allowed | open |
Project status
open — no natural-language proof or Lean formalization yet. See Contribute for pointers if you want to attack this case.