The McKay Conjecture on character degrees | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: M. Cabanes and B. Späth, `The McKay Conjecture on character degrees`, Annals of Math, 203 (3) 2026. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2026-203-3-McKayConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 (hℓ : ℓ.Prime) (S : Sylow ℓ X) :
    (McKayConjecture.Irr' ℓ X).ncard = (McKayConjecture.Irr' ℓ (normalizer S : Subgroup X)).ncard := byℓ:ℕX:Type u_1inst✝¹:Group Xinst✝:Finite Xhℓ:Nat.Prime ℓS:Sylow ℓ X⊢ (Irr' ℓ X).ncard = (Irr' ℓ ↥(normalizer ↑S)).ncard
  sorryAll goals completed! 🐙