19.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

13 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 19

The Erdős–Faber–Lovász conjecture: if $G$ is an edge-disjoint union of $n$ copies of $K_n$, is $\chi(G) = n$?

We model $G$ by a family of $n$ vertex sets of size $n$ (the copies of $K_n$) which pairwise share at most one vertex and which cover the vertex type. Two copies of $K_n$ are edge-disjoint exactly when their vertex sets share at most one vertex.

References:

erdosproblems.com/19
[Hi81] Hindman, N., On a conjecture of Erdős, Faber, and Lovász about $n$-colorings. Canad. J. Math. (1981).
[Ka92] Kahn, J., Coloring nearly-disjoint hypergraphs with $n + o(n)$ colors. J. Combin. Theory Ser. A (1992).
[KKKMO21] Kang, D. Y., Kelly, T., Kühn, D., Methuku, A. and Osthus, D., A proof of the Erdős–Faber–Lovász conjecture. Ann. of Math. (2023). arXiv:2101.04698

Imports (1)

FormalConjecturesUtil

structure Erdos19.EFLConfig A configuration of n pairwise edge-disjoint copies of $K_n$ covering the vertex type V line 49 source
Source documentation
A configuration of n pairwise edge-disjoint copies of $K_n$ covering the vertex type V.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
```
structure EFLConfig (V : Type*) (n : ℕ) where
…
```
def Erdos19.EFLConfig.graph The union graph: distinct vertices are adjacent iff they lie in a common clique line 64 source
Source documentation
The union graph: distinct vertices are adjacent iff they lie in a common clique.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, SimpleGraph
Proof uses: SimpleGraph.mk, And, Ne, Exists, Fin, Membership.mem, Finset, Erdos19.EFLConfig.A
4 instances, coercions and auxiliary constants left out.
```
def graph : SimpleGraph V where
…
```
def Erdos19.EFLConfig.IsShared A vertex is shared if it lies in two different cliques line 70 source
Source documentation
A vertex is shared if it lies in two different cliques.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig
Proof uses: Exists, Fin, And, Ne, Membership.mem, Finset, Erdos19.EFLConfig.A
2 instances, coercions and auxiliary constants left out.
```
def IsShared (v : V) : Prop := ∃ i j, i ≠ j ∧ v ∈ C.A i ∧ v ∈ C.A j
…
```
def Erdos19.EFLConfig.sharedSet The finite set of shared vertices line 74 source
Source documentation
The finite set of shared vertices.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, Finset
Proof uses: Finset.filter, Erdos19.EFLConfig.IsShared, Classical.propDecidable, Finset.biUnion, Fin, Eq, Finset.univ, Erdos19.EFLConfig.A
1 instances, coercions and auxiliary constants left out.
```
noncomputable def sharedSet : Finset V :=
…
```
theorem Erdos19.EFLConfig.le_chromaticNumber The graph $G$ contains a copy of $K_n$, so $n \le \chi(G)$ line 79 source
Source documentation
The graph $G$ contains a copy of $K_n$, so $n \le \chi(G)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, LE.le, ENat, SimpleGraph.chromaticNumber, Erdos19.EFLConfig.graph
Proof uses: Eq, OfNat.ofNat, GT.gt, Or, Nat.eq_zero_or_pos, of_eq_true, Eq.trans, True, congrFun', congrArg, CharP.cast_eq_zero, Eq.symm, SimpleGraph.IsClique, Finset, Erdos19.EFLConfig.A, Fin.mk, Membership.mem, Set, Ne, And.intro and 8 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem le_chromaticNumber : (n : ℕ∞) ≤ C.graph.chromaticNumber := by
…
```
lemma Erdos19.EFLConfig.eq_of_not_shared A vertex that is not shared lies in exactly one clique line 90 source
Source documentation
A vertex that is not shared lies in exactly one clique.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, Not, Erdos19.EFLConfig.IsShared, Fin, Membership.mem, Finset, Erdos19.EFLConfig.A, Eq
Proof uses: Decidable.byContradiction, Exists.intro, Exists, And, Ne, And.intro
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma eq_of_not_shared {v : V} (hv : ¬ C.IsShared v) {i j : Fin n}
    (hi : v ∈ C.A i) (hj : v ∈ C.A j) : i = j := by
…
```
theorem Erdos19.EFLConfig.colorable_of_sharedColoring If the shared vertices can be coloured with $n$ colours so that shared vertices in a common clique get distinct colours, then $G$ is $n$-colourable line 99 source
Source documentation
If the shared vertices can be coloured with $n$ colours so that shared vertices in a common clique get distinct colours, then $G$ is $n$-colourable.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, Fin, Membership.mem, Finset, Erdos19.EFLConfig.A, Erdos19.EFLConfig.IsShared, Eq, SimpleGraph.Colorable, Erdos19.EFLConfig.graph
Proof uses: Finset.filter, Not, Classical.propDecidable, SDiff.sdiff, Finset.univ, Finset.image, LE.le, Finset.card, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, Erdos19.EFLConfig.card_eq, Finset.card_filter_add_card_filter_not, Finset.card_image_le, HSub.hSub, of_eq_true, Eq.trans, True and 42 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 54 steps
Open to load the checked before-and-after goal states.
```
theorem colorable_of_sharedColoring (c : V → Fin n)
    (hc : ∀ i u v, u ∈ C.A i → v ∈ C.A i → C.IsShared u → C.IsShared v → c u = c v → u = v) :
    C.graph.Colorable n := by
…
```
Mentions: c
theorem Erdos19.EFLConfig.card_sharedSet_le There are at most $\binom{n}{2}$ shared vertices, since two cliques share at most one vertex line 155 source
Source documentation
There are at most $\binom{n}{2}$ shared vertices, since two cliques share at most one vertex.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, LE.le, Finset.card, Erdos19.EFLConfig.sharedSet, Nat.choose, OfNat.ofNat
Proof uses: Finset, Fin, dite, Erdos19.EFLConfig.IsShared, Classical.propDecidable, Insert.insert, Classical.choose, Exists, And, Ne, Membership.mem, Erdos19.EFLConfig.A, Singleton.singleton, Classical.choose_spec, Not, EmptyCollection.emptyCollection, Finset.powersetCard, Finset.univ, And.right, Finset.biUnion and 42 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
theorem card_sharedSet_le : C.sharedSet.card ≤ n.choose 2 := by
…
```
theorem Erdos19.erdos_19 If $G$ is an edge-disjoint union of $n$ copies of $K_n$, then is $\chi(G) = n$? sorry line 195 source
Source documentation
If $G$ is an edge-disjoint union of $n$ copies of $K_n$, then is $\chi(G) = n$?

depends on sorry what this means
Statement uses: Iff, True, Nat, Erdos19.EFLConfig, Eq, ENat, SimpleGraph.chromaticNumber, Erdos19.EFLConfig.graph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_19 : answer(sorry) ↔
    ∀ (V : Type) (n : ℕ) (C : EFLConfig V n), C.graph.chromaticNumber = n := by
…
```
Mentions: Erdos19.EFLConfig
theorem Erdos19.erdos_19.variants.le_three The Erdős–Faber–Lovász conjecture holds for $n \le 3$ line 204 source
Source documentation
The Erdős–Faber–Lovász conjecture holds for $n \le 3$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Erdos19.EFLConfig, LE.le, OfNat.ofNat, Eq, ENat, SimpleGraph.chromaticNumber, Erdos19.EFLConfig.graph
Proof uses: le_antisymm, SimpleGraph.Colorable.chromaticNumber_le, Finset.card, Erdos19.EFLConfig.sharedSet, Nat.choose, Erdos19.EFLConfig.card_sharedSet_le, dite, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, Nat.rawCast, Mathlib.Tactic.IntervalCases.of_le_right, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_ofNat, Not, Nat.ge_of_not_lt and 40 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_19.variants.le_three {V : Type*} {n : ℕ} (C : EFLConfig V n) (hn : n ≤ 3) :
    C.graph.chromaticNumber = n := by
…
```
Mentions: Erdos19.EFLConfig
theorem Erdos19.erdos_19.variants.lt_ten Hindman [Hi81] proved the Erdős–Faber–Lovász conjecture for $n < 10$ sorry line 230 source
Source documentation
Hindman [Hi81] proved the Erdős–Faber–Lovász conjecture for $n < 10$.

depends on sorry what this means
Statement uses: Nat, Erdos19.EFLConfig, LT.lt, OfNat.ofNat, Eq, ENat, SimpleGraph.chromaticNumber, Erdos19.EFLConfig.graph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_19.variants.lt_ten :
    ∀ (V : Type) (n : ℕ) (C : EFLConfig V n), n < 10 → C.graph.chromaticNumber = n := by
…
```
Mentions: Erdos19.EFLConfig
theorem Erdos19.erdos_19.variants.kahn Kahn [Ka92] proved that $\chi(G) \le (1 + o(1))n$ sorry line 238 source
Source documentation
Kahn [Ka92] proved that $\chi(G) \le (1 + o(1))n$.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Erdos19.EFLConfig, SimpleGraph.Colorable, Erdos19.EFLConfig.graph, Nat.floor, HMul.hMul, HAdd.hAdd, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_19.variants.kahn :
    ∀ ε > (0 : ℝ), ∀ᶠ n in atTop, ∀ (V : Type) (C : EFLConfig V n),
      C.graph.Colorable ⌊(1 + ε) * n⌋₊ := by
…
```
Mentions: Erdos19.EFLConfig
theorem Erdos19.erdos_19.variants.large_n Kang, Kelly, Kühn, Methuku and Osthus [KKKMO21] proved the Erdős–Faber–Lovász conjecture for all sufficiently large $n$ sorry line 248 source
Source documentation
Kang, Kelly, Kühn, Methuku and Osthus [KKKMO21] proved the Erdős–Faber–Lovász conjecture for all sufficiently large $n$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, Erdos19.EFLConfig, Eq, ENat, SimpleGraph.chromaticNumber, Erdos19.EFLConfig.graph, Filter.atTop
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_19.variants.large_n :
    ∀ᶠ n in atTop, ∀ (V : Type) (C : EFLConfig V n), C.graph.chromaticNumber = n := by
…
```
Mentions: Erdos19.EFLConfig