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 statement3 of 6

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.

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

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

SolvedStatement only, no proof

Sources

Search problems.science