Skip to content

Erdős problem 1092

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1092.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/1092.leanErdos1092.f_asymptotic_general1 lineExact file
False ↔ ∀ (r : ℕ), (fun n => ↑r * ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f r n)
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page