Erdős problem 1092
Is it true that ? Disproved by Rödl, who showed for all fixed . A conjecture of Erdős, Hajnal, and Szemerédi.
Sources
FormalConjectures/ErdosProblems/
1092.lean
Retained formal statement
Is it true that ? Disproved by Rödl, who showed for all fixed . A conjecture of Erdős, Hajnal, and Szemerédi.
This seems to be closely related to, but distinct from, [744](https://www.erdosproblems.com/744).
Tang notes in the comments that Rödl [Ro82] constructed, for any and , a graph with chromatic number such that every graph on vertices is bipartite after deleting at most edges.
False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)SolvedStatement only, no proof