Erdős problem 533 · problems.science

Let $\delta > 0$ . If $n$ is sufficiently large and $G$ is a graph on $n$ vertices with no $K_5$ and at least $\delta n^2$ edges, must $G$ contain a set of $\gg_\delta n$ vertices spanning no triangle?

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

533.lean

Retained formal statement5 of 6

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.

FormalConjectures/ErdosProblems/533.leanErdos533.erdos_533.variants.lrss_lower8 linesExact file

1∀ (ε δ : ℝ),2  0 < ε →3    0 < δ →4      ∀ᶠ (n : ℕ) in Filter.atTop,5        ∃ G,6          G.CliqueFree 5 ∧7            (∀ (S : Finset (Fin n)), G.CliqueFreeOn (↑S) 3 → ↑S.card ≤ δ * ↑n) ∧8              (1 / 12 - ε) * ↑n ^ 2 ≤ ↑G.edgeFinset.card

SolvedStatement only, no proof

Sources

Search problems.science