Erdős problem 579
Let . If is sufficiently large and is a graph on vertices with no (the octahedron) and at least edges, must contain an independent set of size ?
Sources
FormalConjectures/ErdosProblems/
579.lean
Retained formal statement
Sanity check that the forbidden structure is non-trivial: the octahedron is of course not octahedron-free, since it contains a copy of itself.
¬Erdos579.octahedron.Free Erdos579.octahedronTestStatement only, no proof