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 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

Sources

Search problems.science