Erdős problem 812
Burr, Erdős, Faudree, and Schelp [BEFS89] proved that for all .
Sources
FormalConjectures/ErdosProblems/
812.lean
Retained formal statement
Is it true that ?
True ↔ (fun n => ↑n ^ 2) =O[Filter.atTop] fun n => ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) - ↑(Combinatorics.hypergraphRamsey 2 n)OpenStatement only, no proof