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