Erdős problem 1092

Is it true that $f_2(n) \gg n$ ? Disproved by Rödl, who showed $f_r(n) = o(n)$ for all fixed $r \geq 2$ . A conjecture of Erdős, Hajnal, and Szemerédi.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1092.lean

Retained formal statement2 of 2

More generally, is $f_r(n)\gg_r n$ ? Disproved by Rödl, who showed $f_r(n) = o(n)$ for all fixed $r \geq 2$ .

FormalConjectures/ErdosProblems/1092.leanErdos1092.f_asymptotic_general1 lineExact file

1False ↔ ∀ (r : ℕ), (fun n => ↑r * ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f r n)

SolvedStatement only, no proof