The spread of a finite group | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: T. C. Burness, R. M. Guralnick, and S. Harper, `The spread of a finite group`, Annals of Math, 193 (2) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2021-193-2-SpreadOfAFiniteGroup.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1 (G : Type*) [Group G] [Finite G] :
    s G ≥ 2 ↔ ∀ (N : Subgroup G) [N.Normal] [Nontrivial N], IsCyclic (G ⧸ N) := byG:Type u_1inst✝¹:Group Ginst✝:Finite G⊢ s G ≥ 2 ↔ ∀ (N : Subgroup G) [inst : N.Normal] [Nontrivial ↥N], IsCyclic (G ⧸ N)
  sorryAll goals completed! 🐙