750.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

10 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 750

References:

erdosproblems.com/750
[EHS82] Erdős, P. and Hajnal, A. and Szemerédi, E., On almost bipartite large chromatic graphs. Theory and practice of combinatorics (1982), 117-123.
[Er69b] Erdős, P., Problems and results in chromatic graph theory. Proof Techniques in Graph Theory (1969), 27-35.
[Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.
[Er95d] Erdős, Paul, On some problems in combinatorial set theory. Publ. Inst. Math. (Beograd) (N.S.) (1995), 61-65.
[ErHa67b] Erdős, P. and Hajnal, András, On chromatic graphs. Mat. Lapok (1967), 1--4.
UlamErdos750
[St85] Stiebitz, M., Beiträge zur Theorie der färbungskritischen Graphen. Habilitation, TH Ilmenau (1985).
[SaSt89] Sachs, H. and Stiebitz, M., On constructive methods in the theory of colour-critical graphs. Discrete Math. (1989), 287-296.
[MuSt19] Müller, T. and Stehlík, M., Generalised Mycielski graphs and the Borsuk-Ulam theorem. Electron. J. Combin. (2019), P4.8.

Imports (1)

FormalConjecturesUtil

abbrev Erdos750.MycVerts Vertices of the generalised Mycielskian $M_s(G)$: $s$ copies of the vertices of $G$, one per level, and a single apex line 55 source
Source documentation
Vertices of the generalised Mycielskian $M_s(G)$: $s$ copies of the vertices of $G$, one per level, and a single apex.

no axioms what this means
Statement uses: Nat
Proof uses: Sum, Prod, Fin, Unit
```
abbrev MycVerts (s : ℕ) (V : Type u) : Type u := (Fin s × V) ⊕ Unit
```
def Erdos750.MycAdj Adjacency of the generalised Mycielskian, before SimpleGraph.fromRel packages it as a graph line 65 source
Source documentation
Adjacency of the generalised Mycielskian, before SimpleGraph.fromRel packages it as a graph.
Two level-0 vertices are adjacent when the underlying vertices are; a level-i vertex and a level-i + 1 vertex are adjacent when the underlying vertices are; and the apex is adjacent to every vertex on the top level. The relation is already symmetric and irreflexive, so fromRel changes nothing about it.

no axioms what this means
Statement uses: Nat, SimpleGraph, Erdos750.MycVerts
Proof uses: Erdos750.MycAdj.match_1, Fin, Or, And, Eq, OfNat.ofNat, SimpleGraph.Adj, HAdd.hAdd, Unit, False
4 instances, coercions and auxiliary constants left out.
```
def MycAdj (s : ℕ) {V : Type u} (G : SimpleGraph V) : MycVerts s V → MycVerts s V → Prop
  | Sum.inl (i, u), Sum.inl (j, v) =>
      (i.val = 0 ∧ j.val = 0 ∧ G.Adj u v) ∨ (j.val = i.val + 1 ∧ G.Adj u v) ∨
        (i.val = j.val + 1 ∧ G.Adj u v)
  | Sum.inl (i, _), Sum.inr () => i.val + 1 = s
  | Sum.inr (), Sum.inl (i, _) => i.val + 1 = s
  | Sum.inr (), Sum.inr () => False

/--
The **generalised Mycielskian** $M_s(G)$. $M_2(G)$ is the classical Mycielskian, and $M_1(G)$
adds a vertex joined to everything.
-/
```
Mentions: Erdos750.MycVerts
def Erdos750.genMyc The generalised Mycielskian $M_s(G)$ line 77 source
Source documentation
The generalised Mycielskian $M_s(G)$. $M_2(G)$ is the classical Mycielskian, and $M_1(G)$ adds a vertex joined to everything.

standard axioms: Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Erdos750.MycVerts
Proof uses: SimpleGraph.fromRel, Erdos750.MycAdj
```
def genMyc (s : ℕ) {V : Type u} (G : SimpleGraph V) : SimpleGraph (MycVerts s V) :=
…
```
Mentions: Erdos750.MycVerts
theorem Erdos750.genMyc_apex_adj_top The apex of $M_s(G)$ is adjacent to every vertex on the top level line 82 source
Source documentation
The apex of $M_s(G)$ is adjacent to every vertex on the top level.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, LT.lt, OfNat.ofNat, SimpleGraph.Adj, Erdos750.MycVerts, Erdos750.genMyc, Sum.inr, Prod, Fin, Unit, Unit.unit, Sum.inl, Prod.mk, Fin.mk, HSub.hSub
Proof uses: And.intro, Ne, Or, Erdos750.MycAdj, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, eq_false', False.elim, noConfusion_of_Nat, Sum, Sum.ctorIdx, not_false_eq_true, Or.inl, id, Decidable.byContradiction and 1 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem genMyc_apex_adj_top {V : Type u} (G : SimpleGraph V) (s : ℕ) (hs : 0 < s) (v : V) :
    (genMyc s G).Adj (Sum.inr ()) (Sum.inl (⟨s - 1, by omega⟩, v)) := by
…
```
Mentions: Erdos750.genMyc
theorem Erdos750.genMyc_adj_level_zero Two level-0 vertices of $M_s(G)$ are adjacent exactly when the underlying vertices are line 90 source
Source documentation
Two level-0 vertices of $M_s(G)$ are adjacent exactly when the underlying vertices are.

standard axioms: Quot.sound, propext what this means
Statement uses: SimpleGraph, Nat, LT.lt, OfNat.ofNat, SimpleGraph.Adj, Erdos750.MycVerts, Erdos750.genMyc, Sum.inl, Prod, Fin, Unit, Prod.mk, Fin.mk
Proof uses: And.intro, Ne, Or, Erdos750.MycAdj, Eq.mpr, Not, Eq, id, congrArg, Eq.trans, Sum, Sum.inl.injEq, And, Prod.mk.injEq, True, congrFun', eq_self, true_and, SimpleGraph.Adj.ne, Or.inl and 2 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem genMyc_adj_level_zero {V : Type u} (G : SimpleGraph V) {s : ℕ} (hs : 0 < s) {u v : V}
    (huv : G.Adj u v) :
    (genMyc s G).Adj (Sum.inl (⟨0, hs⟩, u)) (Sum.inl (⟨0, hs⟩, v)) := by
…
```
Mentions: Erdos750.genMyc

def Erdos750.IsRecursivelyBuiltMr G belongs to the class $M_r$, meaning it is built from $K_2$ by $r - 2$ generalised Mycielskians line 101 source

Source documentation

G belongs to the class $M_r$, meaning it is built from $K_2$ by $r - 2$ generalised Mycielskians. Stiebitz's theorem is about this class and not about arbitrary graphs: it is false that $\chi(M_s(H)) = \chi(H) + 1$ for every $H$ and every $s$.

standard axioms: Classical.choice, Quot.sound, propext what this means

Statement uses: Nat, SimpleGraph

2 instances, coercions and auxiliary constants left out.

def IsRecursivelyBuiltMr : ∀ (_r : ℕ) {_V : Type u} (_G : SimpleGraph _V), Prop
  | 0, _, _ => False
  | 1, _, _ => False
  | 2, _, G => Nonempty (G ≃g completeGraph (Fin 2))
  | r + 3, _, G => ∃ (W : Type u) (H : SimpleGraph W) (s : ℕ),
      1 ≤ s ∧ IsRecursivelyBuiltMr (r + 2) H ∧ Nonempty (G ≃g genMyc s H)

/--
**Stiebitz's theorem** [St85]: every graph in $M_r$ has chromatic number at least $r$. The
matching upper bound follows from the construction, so the chromatic number is exactly $r$.

This is stated ahead of `erdos_750` because the formal proof linked there assumes it, and the
…

Mentions: Erdos750.genMyc, Erdos750.erdos_750

theorem Erdos750.erdos_750.variants.stiebitz Stiebitz's theorem [St85]: every graph in $M_r$ has chromatic number at least $r$ sorry line 116 source
Source documentation
Stiebitz's theorem [St85]: every graph in $M_r$ has chromatic number at least $r$. The matching upper bound follows from the construction, so the chromatic number is exactly $r$.
This is stated ahead of erdos_750 because the formal proof linked there assumes it, and the assuming clause must name a declaration that already exists. See also [SaSt89] and [MuSt19].

depends on sorry what this means
Statement uses: SimpleGraph, Nat, Erdos750.IsRecursivelyBuiltMr, LE.le, ENat, SimpleGraph.chromaticNumber
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_750.variants.stiebitz {V : Type u} (G : SimpleGraph V) (r : ℕ)
    (h : IsRecursivelyBuiltMr r G) : (r : ℕ∞) ≤ G.chromaticNumber := by
…
```
Mentions: Erdos750.IsRecursivelyBuiltMr
theorem Erdos750.erdos_750 sorry line 135 source
depends on sorry what this means
Statement uses: Iff, True, Nat, NNReal, Filter.Tendsto, Filter.atTop, Exists, SimpleGraph, And, Eq, ENat, SimpleGraph.chromaticNumber, Top.top, Set, LT.lt, OfNat.ofNat, Set.ncard, LE.le, SimpleGraph.IsIndepSet, HSub.hSub and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos750.erdos_750.variants.epsilon In [Er69b] Erdős conjectures this for $f(m)=\epsilon m$ for any fixed $\epsilon>0$ sorry line 147 source
Source documentation
In [Er69b] Erdős conjectures this for $f(m)=\epsilon m$ for any fixed $\epsilon>0$. This follows from a result of Erdős, Hajnal, and Szemerédi [EHS82], as described by Sellke in the comments.

depends on sorry what this means
Statement uses: Iff, True, NNReal, GT.gt, OfNat.ofNat, Exists, SimpleGraph, And, Eq, ENat, SimpleGraph.chromaticNumber, Top.top, Nat, Set, LT.lt, Set.ncard, LE.le, SimpleGraph.IsIndepSet, HSub.hSub, HDiv.hDiv and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_750.variants.epsilon :
    answer(True) ↔ ∀ (ε : ℝ≥0), ε > 0 →
      ∃ (V : Type*) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
          ∃ I ⊆ S, G.IsIndepSet I ∧ m / 2 - ε * m ≤ I.ncard := by
…
```
theorem Erdos750.erdos_750.variants.c_gt_quarter In [ErHa67b] Erdős and Hajnal prove this for $f(m)\geq cm$ for all $c>1/4$ sorry line 158 source
Source documentation
In [ErHa67b] Erdős and Hajnal prove this for $f(m)\geq cm$ for all $c>1/4$.

depends on sorry what this means
Statement uses: Iff, True, NNReal, GT.gt, HDiv.hDiv, OfNat.ofNat, Nat, Exists, SimpleGraph, And, Eq, ENat, SimpleGraph.chromaticNumber, Top.top, Set, LT.lt, Set.ncard, LE.le, SimpleGraph.IsIndepSet, HSub.hSub and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
52 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_750.variants.c_gt_quarter :
    answer(True) ↔ ∀ (c : ℝ≥0), c > 1 / 4 →
      ∃ (V : Type*) (G : SimpleGraph V), G.chromaticNumber = ⊤ ∧
        ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m →
          ∃ I ⊆ S, G.IsIndepSet I ∧ m / 2 - c * m ≤ I.ncard := by
…
```
Mentions: c