Formal target: Corpus.WikipediaDiameterSimpleFiniteGroups.babai_seress_conjecture_alternating

**Babai–Seress Conjecture (Conjecture 1.5)**: There exists an absolute constant $C$ such that the diameter of the alternating group $A_n$ satisfies $$\operatorname{diam}(A_n) \leq n^C.$$ *Reference:* [L.

Exact formal statement

Exists.{1} fun C =>
  ∀ (n : Nat),
    LE.le.{0}
      (Nat.cast.{0}
        (Corpus.WikipediaDiameterSimpleFiniteGroups.groupDiam.{0}
          (Subtype.{1} fun x => Membership.mem.{0, 0} (alternatingGroup.{0} (Fin n)) x)))
      (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) C)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record