Order 50 = 2 · 5²

From the paper (Macaj–Siran 2010)

Theorem 7 lists 50 as a surviving even-order maximum. But Theorem 2 (Makhnev–Paduchikh) combined with Proposition 3 excludes most groups of this order:

• Theorem 2 requires |Y| ∈ {1, 3, 5, 7, 19, 21, 57}, so |Y| = 25 is impossible — this excludes D₂₅ and the full-inversion (ℤ₅)² ⋊ ℤ₂.
• For |Y| = 1 the remaining odd part has |X| = 25; Theorem 2(b) requires Fix(X) ∈ {star, pentagon, Petersen, HS}. Pentagon needs |X| ∣ 55 (fails) and HS forces |X| ≤ 5 (Proposition 3) — both impossible. So ℤ₅₀ and ℤ₂ × (ℤ₅)² are paper-excluded.
• The only allowed decomposition is |Y| = 5, |X| = 5, giving D₅ × ℤ₅ as the unique paper-allowed group at this order.

Natural-language proof (this project)

not yet written

Strategy: a Sylow-5 subgroup of G of order 25 is one of two abelian types (ℤ₂₅ or ℤ₅ × ℤ₅), each with a fixed-point set isomorphic to a sub-structure of the Hoffman–Singleton graph; the involution then has a₀ = 56 and a₁ = 112 (Lemma 2). Combining these should close all five SmallGroup cases. See Contribute.

Lean formalization (this project)

open

Group classification (SmallGroup(50, k))

GAP SmallGroup IDs are illustrative; paper-status is determined by isomorphism class.