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

4 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 615

A Ramsey–Turán problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS93]: does there exist a constant $c > 0$ such that every graph on $n$ vertices with at least $(1/8 - c)n^2$ edges contains either a $K_4$ or an independent set on at least $n/\log n$ vertices? In the notation of Ramsey–Turán theory this asks whether $$\mathrm{rt}(n; 4, n/\log n) < (1/8 - c)n^2.$$

This was disproved by Fox, Loh, and Zhao [FLZ15], who showed that $\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2$ whenever $f(n) = o(\sqrt{\log n/\log\log n})$. In the other direction Sudakov [Su03] had shown that $\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)$ whenever $f(n)/\sqrt{\log n} \to \infty$.

References:

erdosproblems.com/615
[EHSSS93] Erdős, P., Hajnal, A., Simonovits, M., Sós, V. T., and Szemerédi, E., Turán-Ramsey theorems and simple asymptotically extremal structures. Combinatorica 13 (1993), 31--56.
[Su03] Sudakov, B., A few remarks on Ramsey-Turán-type problems. J. Combin. Theory Ser. B 88 (2003), 99--106.
[FLZ15] Fox, J., Loh, P.-S., and Zhao, Y., The critical window for the classical Ramsey-Turán problem. Combinatorica 35 (2015), 435--476.

Imports (1)

FormalConjecturesUtil

theorem Erdos615.erdos_615 sorry line 61 source
depends on sorry what this means
Statement uses: Iff, False, Exists, Real, And, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, SimpleGraph, Fin, LE.le, HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, Finset.card, Sym2, SimpleGraph.edgeFinset, Classical.propDecidable and 7 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
54 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Erdos615.erdos_615.variants.fox_loh_zhao Documented declaration: fox_loh_zhao sorry line 78 source
Source documentation
The result of Fox, Loh, and Zhao [FLZ15] disproving the problem: if $f(n) \geq 0$ satisfies $f(n) = o(\sqrt{\log n/\log\log n})$, then for every $\epsilon > 0$ and all sufficiently large $n$ there is a $K_4$-free graph on $n$ vertices with independence number at most $ne^{-f(n)}$ and at least $(1/8 - \epsilon)n^2$ edges; that is, $\mathrm{rt}(n; 4, ne^{-f(n)}) \geq (1/8 - o(1))n^2$. Applied with $f(n) = \log\log n$, this disproves the headline problem, since $ne^{-f(n)} = n/\log n = o(n)$.

depends on sorry what this means
Statement uses: Nat, Real, LE.le, OfNat.ofNat, Filter.Tendsto, HDiv.hDiv, Real.sqrt, Real.log, Filter.atTop, nhds, LT.lt, Filter.Eventually, Exists, SimpleGraph, Fin, And, SimpleGraph.CliqueFree, SimpleGraph.indepNum, HMul.hMul, Real.exp and 8 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_615.variants.fox_loh_zhao (f : ℕ → ℝ) (hf : ∀ n, 0 ≤ f n)
    (hfo : Tendsto (fun n : ℕ => f n / Real.sqrt (Real.log n / Real.log (Real.log n)))
      atTop (nhds 0)) (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ (n : ℕ) in atTop,
      ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
        (G.indepNum : ℝ) ≤ n * Real.exp (-f n) ∧
        (1 / 8 - ε) * n ^ 2 ≤ G.edgeFinset.card := by
…
```
theorem Erdos615.erdos_615.variants.sudakov Documented declaration: sudakov sorry line 95 source
Source documentation
The complementary result of Sudakov [Su03]: if $f(n)/\sqrt{\log n} \to \infty$ then $\mathrm{rt}(n; 4, ne^{-f(n)}) = o(n^2)$; that is, for every $\epsilon > 0$ and all sufficiently large $n$, every $K_4$-free graph on $n$ vertices with independence number at most $ne^{-f(n)}$ has at most $\epsilon n^2$ edges.

depends on sorry what this means
Statement uses: Nat, Real, Filter.Tendsto, HDiv.hDiv, Real.sqrt, Real.log, Filter.atTop, LT.lt, OfNat.ofNat, Filter.Eventually, SimpleGraph, Fin, SimpleGraph.CliqueFree, LE.le, SimpleGraph.indepNum, HMul.hMul, Real.exp, Neg.neg, Finset.card, Sym2 and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_615.variants.sudakov (f : ℕ → ℝ)
    (hf : Tendsto (fun n : ℕ => f n / Real.sqrt (Real.log n)) atTop atTop)
    (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ (n : ℕ) in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
        (G.indepNum : ℝ) ≤ n * Real.exp (-f n) →
        (G.edgeFinset.card : ℝ) ≤ ε * n ^ 2 := by
…
```
theorem Erdos615.erdos_615.variants.test_bot Documented declaration: test_bot line 110 source
Source documentation
A sanity check for erdos_615: the empty graph on $n \geq 3$ vertices contains an independent set on at least $n/\log n$ vertices (namely the whole vertex set), so it satisfies the conclusion of the implication in the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, HDiv.hDiv, Real.log, SimpleGraph.indepNum, Fin, Bot.bot, SimpleGraph
Proof uses: cast, Eq.symm, Eq.mpr, Real.exp, id, Eq, congrArg, propext, Real.le_log_iff_exp_le, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, LT.lt, HAdd.hAdd, HMul.hMul, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow and 120 more
138 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_615.variants.test_bot (n : ℕ) (hn : 3 ≤ n) :
    (n : ℝ) / Real.log n ≤ (⊥ : SimpleGraph (Fin n)).indepNum := by
…
```