Formal target: Corpus.PaperConjugacyClassSizes.conjClassSizes_iff_sym_three

**Markel's $S_3$-conjecture** (1973): any nontrivial finite ah-group is isomorphic to $S_3$.

Exact formal statement

∀ (G : Type) [inst : Group.{0} G] [inst_1 : Fintype.{0} G] [Nontrivial.{0} G],
  Corpus.PaperConjugacyClassSizes.HasDistinctConjClassSizes.{0} G →
    Nonempty.{1} (MulEquiv.{0, 0} G (Equiv.Perm.{1} (Fin 3)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record