Erdős problem 533

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

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

533.lean

Retained formal statement6 of 6

Sanity check for the triangle-free-set condition: in the empty graph every vertex set spans no triangle, since the empty graph has no $3$ -clique.

FormalConjectures/ErdosProblems/533.leanErdos533.erdos_533.variants.test_bot1 lineExact file

1∀ (n : ℕ) (S : Finset (Fin n)), ⊥.CliqueFreeOn (↑S) 3

TestStatement only, no proof