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 for some constant , for all large ?
True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + cOpenStatement only, no proof