Erdős problem 533
Let . If is sufficiently large and is a graph on vertices with no and at least edges, must contain a set of vertices spanning no triangle?
Sources
FormalConjectures/ErdosProblems/
533.lean
Let . If is sufficiently large and is a graph on vertices with no and at least edges, must contain a set of vertices spanning no triangle?
Equivalently, writing for the maximum number of edges of a -free graph on vertices in which every triangle-free vertex set has fewer than vertices (the *triangle Ramsey–Turán number*), is
This is a problem of Erdős, Hajnal, Simonovits, Sós, and Szemerédi [EHSSS94], who proved and the analogous , and observed via a construction of Erdős and Rogers [ErRo62].
The answer is no: Balogh and Lenz [BaLe13] disproved it by showing , and the exact value was determined by the matching lower-bound construction of Liu, Reiher, Sharifzadeh, and Staden [LRSS21] (see erdos_533.variants.lrss_lower).
False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3