Erdős–Faber–Lovász conjecture

AbbreviationHypergraph#✓fully proved

A hypergraph on a type \(V\) of vertices is a set of subsets of \(V\); its elements are the edges of the hypergraph. Edges may be empty, and no finiteness condition is imposed.

abbrev Hypergraph (V : Type*) := Set (Set V)

Used by 4

Used byChromatic index of a hypergraph · Edge coloring of a hypergraph · Linear hypergraph · Erdős–Faber–Lovász conjecture for sufficiently many vertices

StructureEdge coloring of a hypergraph#✓fully proved

Let \(\mathcal{H}\) be a hypergraph on a vertex type \(V\) and let \(\alpha\) be a type. An \(\alpha\)-coloring of \(\mathcal{H}\) is a map \(c\) from the set of edges of \(\mathcal{H}\) to \(\alpha\) such that \(c(e_1) \ne c(e_2)\) for any two distinct edges \(e_1\) and \(e_2\) of \(\mathcal{H}\) that have a vertex in common.

structure Hypergraph.Coloring (α : Type*) (𝓗 : Hypergraph V) where
  /-- The labeling of a hypergraph coloring. -/
  labels : 𝓗 → α
  isColoring (e₁ e₂ : 𝓗) (h : e₁ ≠ e₂) (h' : (e₁ ∩ e₂ : Set V).Nonempty) : labels e₁ ≠ labels e₂

Uses 1 · Used by 1

Statement usesHypergraph

Used byChromatic index of a hypergraph

DefinitionLinear hypergraph#✓fully proved

A hypergraph \(\mathcal{H}\) is linear if any two distinct edges of \(\mathcal{H}\) have at most one vertex in common.

def Hypergraph.IsLinear (𝓗 : Hypergraph V) :=
  𝓗.Pairwise fun e₁ e₂ ↦ (e₁ ∩ e₂).Subsingleton

Uses 1 · Used by 1

Statement usesHypergraph

Used byErdős–Faber–Lovász conjecture for sufficiently many vertices

DefinitionChromatic index of a hypergraph#✓fully proved

The chromatic index of a hypergraph \(\mathcal{H}\) is the least natural number \(n\) such that \(\mathcal{H}\) has a coloring with colors in \(\{0, 1, \dots, n-1\}\), and \(0\) if there is no such \(n\).

noncomputable def Hypergraph.chromaticIndex (𝓗 : Hypergraph V) : ℕ :=
  sInf {n : ℕ | Nonempty (𝓗.Coloring (Fin n))}

Uses 2 · Used by 1

Statement usesHypergraph · Edge coloring of a hypergraph

Used byErdős–Faber–Lovász conjecture for sufficiently many vertices

TheoremErdős–Faber–Lovász conjecture for sufficiently many vertices#●ready to prove

For every sufficiently large natural number \(n\), every linear hypergraph on the vertex set \(\{0, 1, \dots, n-1\}\) has chromatic index at most \(n\).

public theorem_wanted theorem_1_1 :
    ∀ᶠ n in atTop, ∀ 𝓗 : Hypergraph (Fin n), 𝓗.IsLinear → 𝓗.chromaticIndex ≤ n

Sources

• 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. Problem annals_erdos_faber_lovasz_conjecture of the lean-eval benchmark.

Uses 3

Statement usesHypergraph · Linear hypergraph · Chromatic index of a hypergraph

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.