Erdős Problem 812

References:

• erdosproblems.com/812
• [BEFS89] Burr, S. A. and Erd\H{o}s, P. and Faudree, R. J. and Schelp, R. H., On the difference between consecutive {R}amsey numbers. Utilitas Math. (1989), 115--118.

theorem Erdos812.erdos_812.parts.i : True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + c

Is it true that $\frac{R(n+1)}{R(n)}\geq 1+c$ for some constant $c>0$, for all large $n$?

theorem Erdos812.erdos_812.parts.ii : True ↔ (fun (n : ℕ) => ↑n ^ 2) =O[Filter.atTop] fun (n : ℕ) => ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) - ↑(Combinatorics.hypergraphRamsey 2 n)

Is it true that $R(n+1)-R(n) \gg n^2$?

theorem Erdos812.erdos_812.variants.lower_bound (n : ℕ) : n ≥ 2 → ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) - ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 4 * ↑n - 8

Burr, Erdős, Faudree, and Schelp [BEFS89] proved that $R(n+1)-R(n) \geq 4n-8$ for all $n\geq 2$.