erdos_faber_lovasz_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result erdos_faber_lovasz_conjecture is named for, so its Disproved status carries no information about it. Do not import it or use it as a dependency.

Erdős–Faber–Lovász conjecture (1972): If k complete graphs K_k each share at most one vertex pairwise, then the union has chromatic number k. Proved for large k by Kang–Kelly–Kühn–Methuku–Osthus (2021); open for small k.

Why this node was retired

The posted statement is

import Mathlib

theorem erdos_faber_lovasz_conjecture (k : ℕ) (hk : 1 ≤ k)
    (cliques : Fin k → Finset (Fin (k * k)))
    (hsize : ∀ i, cliques i = Finset.univ.filter (fun v => v.val / k = i.val) ∨ True)
    (hpairwise : ∀ i j : Fin k, i ≠ j → (cliques i ∩ cliques j).card ≤ 1) :
    ∃ col : Fin (k * k) → Fin k,
      ∀ i : Fin k, ∀ u ∈ cliques i, ∀ v ∈ cliques i, u ≠ v → col u ≠ col v := by
  sorry

The hypothesis hsize : ∀ i, cliques i = … ∨ True is satisfied by its right disjunct for every family, so cliques is an arbitrary family of finsets rather than the intended complete graphs. The conclusion then asserts a proper k-colouring for arbitrary families, which is false — hence the Disproved status, which says nothing about the conjecture.

What a faithful statement would require

The ∨ True must be dropped so that each cliques i really is a complete graph on k vertices, with the near-disjointness hypothesis as stated.

No corrected replacement node exists yet.