Ramsey–Turán theory

DefinitionEP-533: linear triangle-free sets in dense \(K_5\)-free graphs#✓fully proved

The conjecture states that for every real \(\delta > 0\) there is a real \(c > 0\) such that, for all sufficiently large \(n\), every \(K_5\)-free simple graph on \(n\) vertices with at least \(\delta n^2\) edges has a triangle-free set of at least \(c n\) vertices (a set of vertices no three of which are pairwise adjacent).

def conjecture : Prop :=
  ∀ δ : ℝ, 0 < δ → ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
    ∀ G : SimpleGraph (Fin n), G.CliqueFree 5 →
      δ * (n : ℝ) ^ 2 ≤ G.edgeFinset.card →
        ∃ S : Finset (Fin n), c * (n : ℝ) ≤ (S.card : ℝ) ∧
          G.CliqueFreeOn (S : Set (Fin n)) 3

Used by 1

Used byEP-533 is false: dense \(K_5\)-free graphs without linear triangle-free sets

TheoremEP-533 is false: dense \(K_5\)-free graphs without linear triangle-free sets#●ready to prove

There is a real \(\delta > 0\) such that for every real \(c > 0\) there are infinitely many \(n\) for which some \(K_5\)-free simple graph on \(n\) vertices has at least \(\delta n^2\) edges and yet has no triangle-free set of at least \(c n\) vertices (a set of vertices no three of which are pairwise adjacent). In other words, the EP-533 conjecture fails.

Balogh and Lenz (2011) first gave \(K_5\)-free graphs of positive density with no linear triangle-free set; Liu, Reiher, Sharifzadeh and Staden (Theorem 1.1 with \(p = 3\), \(\ell = 1\)) give \(K_5\)-free graphs on \(2n\) vertices with \((1/3 - o(1))n^2\) edges whose largest triangle-free set has \(o(n)\) vertices, refuting \(\delta = 1/24\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• Hong Liu, Christian Reiher, Maryam Sharifzadeh and Katherine Staden, Geometric constructions for Ramsey–Turán theory, J. Eur. Math. Soc. 28 (2026), arXiv:2103.10423, https://arxiv.org/abs/2103.10423.

Uses 1

Statement usesEP-533: linear triangle-free sets in dense \(K_5\)-free graphs

DefinitionRamsey–Turán problem for \(K_4\) (Erdős Problem 22)#✓fully proved

For a graph \(G\) write \(\alpha(G)\) for its independence number and \(e(G)\) for its number of edges, and call \(G\) \(K_4\)-free if it has no four pairwise adjacent vertices. The statement is the conjunction of the following four assertions.

(i) For every real \(\varepsilon > 0\) and all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \varepsilon n\) and \(e(G) \ge n^2/8\).

(ii) (Szemerédi's upper bound.) For every real \(\varepsilon > 0\) there is a real \(\delta > 0\) such that, for all sufficiently large \(n\), every \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \delta n\) satisfies \(e(G) \le (1/8 + \varepsilon) n^2\).

(iii) (Bollobás–Erdős lower bound.) For all real \(\varepsilon > 0\) and \(\delta > 0\) and all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \delta n\) and \(e(G) \ge (1/8 - \varepsilon) n^2\).

(iv) (Fox–Loh–Zhao quantitative form.) There is a real \(C > 0\) such that, for all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(e(G) \ge n^2/8\) and \(\alpha(G) \le C n (\log \log n)^{3/2} / (\log n)^{1/2}\).

MathlibExt.GraphTheory.ErdosProblem22Wanted.conjecture · 17 lines

def conjecture : Prop :=
  (∀ ε : ℝ, 0 < ε → ∀ᶠ (n : ℕ) in atTop,
    ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
      (G.indepNum : ℝ) ≤ ε * n ∧ (n : ℝ) ^ 2 / 8 ≤ G.edgeFinset.card) ∧
  (∀ (ε : ℝ), 0 < ε →
    ∃ δ : ℝ, 0 < δ ∧ ∀ᶠ (n : ℕ) in atTop,
      ∀ G : SimpleGraph (Fin n), G.CliqueFree 4 →
        (G.indepNum : ℝ) ≤ δ * n →
        (G.edgeFinset.card : ℝ) ≤ (1 / 8 + ε) * n ^ 2) ∧
  (∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∀ᶠ (n : ℕ) in atTop,
    ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
      (G.indepNum : ℝ) ≤ δ * n ∧ (1 / 8 - ε) * n ^ 2 ≤ G.edgeFinset.card) ∧
  (∃ C : ℝ, 0 < C ∧ ∀ᶠ (n : ℕ) in atTop,
    ∃ G : SimpleGraph (Fin n), G.CliqueFree 4 ∧
      (G.indepNum : ℝ) ≤
        C * (Real.log (Real.log n)) ^ (3 / 2 : ℝ) / (Real.log n) ^ (1 / 2 : ℝ) * n ∧
      (n : ℝ) ^ 2 / 8 ≤ G.edgeFinset.card)

Used by 1

Used byResolution of Erdős Problem 22 (Fox–Loh–Zhao)

TheoremThe empty graph meets the Ramsey–Turán edge bound for \(K_4\)#✓fully proved

For every natural number \(n\) and every real \(\varepsilon > 0\), the empty graph on \(n\) vertices has no four pairwise adjacent vertices, and its number of edges (namely \(0\)) is at most \((1/8 + \varepsilon) n^2\).

theorem test_bot (n : ℕ) (ε : ℝ) (hε : 0 < ε) :
    (⊥ : SimpleGraph (Fin n)).CliqueFree 4 ∧
      (((⊥ : SimpleGraph (Fin n)).edgeFinset.card : ℝ)) ≤ (1 / 8 + ε) * n ^ 2

TheoremResolution of Erdős Problem 22 (Fox–Loh–Zhao)#●ready to prove

For a graph \(G\) write \(\alpha(G)\) for its independence number and \(e(G)\) for its number of edges, and call \(G\) \(K_4\)-free if it has no four pairwise adjacent vertices. All four of the following assertions hold.

(i) For every real \(\varepsilon > 0\) and all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \varepsilon n\) and \(e(G) \ge n^2/8\).

(ii) (Szemerédi's upper bound.) For every real \(\varepsilon > 0\) there is a real \(\delta > 0\) such that, for all sufficiently large \(n\), every \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \delta n\) satisfies \(e(G) \le (1/8 + \varepsilon) n^2\).

(iii) (Bollobás–Erdős lower bound.) For all real \(\varepsilon > 0\) and \(\delta > 0\) and all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(\alpha(G) \le \delta n\) and \(e(G) \ge (1/8 - \varepsilon) n^2\).

(iv) (Fox–Loh–Zhao quantitative form.) There is a real \(C > 0\) such that, for all sufficiently large \(n\), there is a \(K_4\)-free graph \(G\) on \(n\) vertices with \(e(G) \ge n^2/8\) and \(\alpha(G) \le C n (\log \log n)^{3/2} / (\log n)^{1/2}\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Jacob Fox, Po-Shen Loh, and Yufei Zhao, The critical window for the classical Ramsey-Turán problem, Combinatorica 35 (2015), 435–476.

Uses 1

Statement usesRamsey–Turán problem for \(K_4\) (Erdős Problem 22)

3 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.