Skip to content

Erdős problem 579

Let δ>0\delta > 0. If nn is sufficiently large and GG is a graph on nn vertices with no K2,2,2K_{2,2,2} (the octahedron) and at least δn2\delta n^2 edges, must GG contain an independent set of size ≫δn\gg_\delta n?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

579.lean

Retained formal statement3 of 3

Sanity check that the forbidden structure is non-trivial: the octahedron is of course not octahedron-free, since it contains a copy of itself.

FormalConjectures/ErdosProblems/579.leanErdos579.erdos_579.variants.octahedron_not_free1 lineExact file
¬Erdos579.octahedron.Free Erdos579.octahedron
TestStatement only, no proof