Burnside p^a q^b theorem | Lean AI formalization leaderboard

Problem statement

Notes: Burnside's theorem that a finite group of order p^a q^b is solvable.

Source: Classical theorem in finite group theory.

Informal solution: Use character theory and induction on the group order to prove solvability.

theorem declaration uses `sorry`finite_group_isSolvable_of_card_eq_prime_pow_mul_prime_pow {G : Type*} [Group G] [Fintype G]
    {p q a b : ℕ}
    (hp : Nat.Prime p)
    (hq : Nat.Prime q)
    (hpq : p ≠ q)
    (hcard : Fintype.card G = p ^ a * q ^ b) :
    Group.IsSolvable G := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gp:ℕq:ℕa:ℕb:ℕhp:Nat.Prime phq:Nat.Prime qhpq:p ≠ qhcard:Fintype.card G = p ^ a * q ^ b⊢ Group.IsSolvable G
  sorryAll goals completed! 🐙