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
More generally, is ? Disproved by Rödl, who showed for all fixed .
False ↔ ∀ (r : ℕ), (fun n => ↑r * ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f r n)SolvedStatement only, no proof