Erdős problem 579

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

This is a problem of Erdős, Hajnal, Sós, and Szemerédi [EHSS83]. It is open; they proved the statement for $\delta > 1/8$ (see erdos_579.variants.ehss_large_delta), and the difficulty is to push the edge-density threshold down to an arbitrary $\delta > 0$.

Here $K_{2,2,2}$ is the complete tripartite graph with all parts of size $2$, encoded as completeMultipartiteGraph (fun _ : Fin 3 => Fin 2); "contains no $K_{2,2,2}$" is expressed via SimpleGraph.Free.