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

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 533

References:

erdosproblems.com/533
[EHSSS94] P. Erdős, A. Hajnal, M. Simonovits, V. T. Sós and E. Szemerédi, Turán-Ramsey theorems and $K_p$-independence numbers, Combin. Probab. Comput. 3 (1994), 297–325.
[ErRo62] P. Erdős and C. A. Rogers, The construction of certain graphs, Canad. J. Math. 14 (1962), 702–707.
[BaLe13] J. Balogh and J. Lenz, On the Ramsey–Turán numbers of graphs and hypergraphs, Israel J. Math. 194 (2013), 45–68.
[LRSS21] H. Liu, C. Reiher, M. Sharifzadeh and K. Staden, Geometric constructions for Ramsey–Turán theory, arXiv:2103.10423 (2021).

Imports (1)

FormalConjecturesUtil

theorem Erdos533.erdos_533 sorry line 65 source
depends on sorry what this means
Statement uses: Iff, False, Real, LT.lt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, SimpleGraph, Fin, SimpleGraph.CliqueFree, LE.le, HMul.hMul, HPow.hPow, Finset.card, Sym2, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos533.erdos_533.variants.ehsss_upper The upper bound sorry line 81 source
Source documentation
The upper bound $\delta_3(5) \leq 1/12$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: for every $\epsilon > 0$ there is a $\delta > 0$ such that for all sufficiently large $n$, every $K_5$-free graph $G$ on $n$ vertices in which every triangle-free vertex set has at most $\delta n$ vertices has at most $(1/12 + \epsilon)n^2$ edges.

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, SimpleGraph, Fin, SimpleGraph.CliqueFree, Finset, SimpleGraph.CliqueFreeOn, LE.le, Finset.card, HMul.hMul, Sym2, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj, HAdd.hAdd and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_533.variants.ehsss_upper (ε : ℝ) (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ n : ℕ in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
        (∀ S : Finset (Fin n),
            G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) →
          (G.edgeFinset.card : ℝ) ≤ (1 / 12 + ε) * n ^ 2 := by
…
```
theorem Erdos533.erdos_533.variants.lrss_lower The matching lower bound sorry line 99 source
Source documentation
The matching lower bound $\delta_3(5) \geq 1/12$, from the construction of Liu, Reiher, Sharifzadeh, and Staden [LRSS21] (improving the earlier $\delta_3(5) > 0$ of Balogh and Lenz [BaLe13]): for every $\epsilon, \delta > 0$ and all sufficiently large $n$ there is a $K_5$-free graph $G$ on $n$ vertices in which every triangle-free vertex set has at most $\delta n$ vertices, yet which has at least $(1/12 - \epsilon)n^2$ edges. In particular this refutes erdos_533.

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Exists, SimpleGraph, Fin, And, SimpleGraph.CliqueFree, Finset, SimpleGraph.CliqueFreeOn, LE.le, Finset.card, HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, Sym2, SimpleGraph.edgeFinset and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_533.variants.lrss_lower (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∀ᶠ n : ℕ in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 5 ∧
        (∀ S : Finset (Fin n),
            G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
        (1 / 12 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card := by
…
```
theorem Erdos533.erdos_533.variants.delta_four_eq_zero The contrasting positive result $\delta_3(4) = 0$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: the $K_4$ analogue of erdos_533 is true sorry line 116 source
Source documentation
The contrasting positive result $\delta_3(4) = 0$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94]: the $K_4$ analogue of erdos_533 is true. For every $\delta > 0$ there is a $c > 0$ such that for all sufficiently large $n$, every $K_4$-free graph $G$ on $n$ vertices with at least $\delta n^2$ edges contains a triangle-free vertex set of size at least $c n$.

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Exists, And, Filter.Eventually, Nat, SimpleGraph, Fin, SimpleGraph.CliqueFree, LE.le, HMul.hMul, HPow.hPow, Finset.card, Sym2, SimpleGraph.edgeFinset, Classical.propDecidable, SimpleGraph.Adj, Finset, SimpleGraph.CliqueFreeOn and 1 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_533.variants.delta_four_eq_zero :
    ∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
        δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
          ∃ S : Finset (Fin n), c * n ≤ (S.card : ℝ) ∧
            G.CliqueFreeOn (S : Set (Fin n)) 3 := by
…
```
Mentions: c
theorem Erdos533.erdos_533.variants.delta_seven_ge_quarter Documented declaration: delta_seven_ge_quarter sorry line 133 source
Source documentation
The observation $\delta_3(7) \geq 1/4$ of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94], via a construction of Erdős and Rogers [ErRo62]: for every $\epsilon, \delta > 0$ and all sufficiently large $n$ there is a $K_7$-free graph $G$ on $n$ vertices in which every triangle-free vertex set has at most $\delta n$ vertices, yet which has at least $(1/4 - \epsilon)n^2$ edges.

depends on sorry what this means
Statement uses: Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Exists, SimpleGraph, Fin, And, SimpleGraph.CliqueFree, Finset, SimpleGraph.CliqueFreeOn, LE.le, Finset.card, HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, Sym2, SimpleGraph.edgeFinset and 3 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
58 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_533.variants.delta_seven_ge_quarter (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    ∀ᶠ n : ℕ in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 7 ∧
        (∀ S : Finset (Fin n),
            G.CliqueFreeOn (S : Set (Fin n)) 3 → (S.card : ℝ) ≤ δ * n) ∧
        (1 / 4 - ε) * (n : ℝ) ^ 2 ≤ G.edgeFinset.card := by
…
```
theorem Erdos533.erdos_533.variants.test_bot Sanity check for the triangle-free-set condition: in the empty graph every vertex set spans no triangle, since the empty graph has no $3$-clique line 146 source
Source documentation
Sanity check for the triangle-free-set condition: in the empty graph every vertex set spans no triangle, since the empty graph has no $3$-clique.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, SimpleGraph.CliqueFreeOn, Bot.bot, SimpleGraph, OfNat.ofNat
Proof uses: LE.le, Set, SimpleGraph.IsNClique, SimpleGraph.cliqueFree_bot, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_533.variants.test_bot (n : ℕ) (S : Finset (Fin n)) :
    (⊥ : SimpleGraph (Fin n)).CliqueFreeOn (S : Set (Fin n)) 3 :=
…
```