Skip to content

Erdős problem 812

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

812.lean

Retained formal statement3 of 3

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

FormalConjectures/ErdosProblems/812.leanErdos812.erdos_812.variants.lower_bound1 lineExact file
∀ n ≥ 2, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) - ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 4 * ↑n - 8
SolvedStatement only, no proof