A proof of the Erdős–Faber–Lovász conjecture | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: D. Y. Kang, T. Kelly, D. Kühn, A. Methuku, and D. Osthus, `A proof of the Erdős–Faber–Lovász conjecture`, Annals of Math, 198 (2) 2023. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2023-198-2-ErdosFaberLovaszConjecture.lean

Informal solution: Unavailable.

theorem declaration uses `sorry`theorem_1_1 :
    ∀ᶠ n in atTop, ∀ 𝓗 : ErdosFaberLovaszConjecture.Hypergraph (Fin n), 𝓗.IsLinear → 𝓗.chromaticIndex ≤ n := by⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (𝓗 : Hypergraph (Fin n)), 𝓗.IsLinear → 𝓗.chromaticIndex ≤ n
  sorryAll goals completed! 🐙