Proof of the simplicity conjecture | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: D. Cristofaro-Gardiner, V. Humilière, and S. Seyfaddini, `Proof of the simplicity conjecture`, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-199-1-SimplicityConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_2 : ¬ IsSimpleGroup SimplicityConjecture.Homeo := by⊢ ¬IsSimpleGroup ↥Homeo
  sorryAll goals completed! 🐙