Erdős problem 1014

Let $R(k,l)$ be the Ramsey number, so the minimal $n$ such that every graph on at least $n$ vertices contains either a $K_k$ or an independent set on $l$ vertices.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1014.lean

Retained formal statement2 of 2

That proof in fact shows that $R(k,l+1)\leq (1+O(l^{-c/k^2}))R(k,l)$ for some constant $c>0$ .

FormalConjectures/ErdosProblems/1014.leanErdos1014.erdos_1014.variants.upper_bound1 lineExact file

1∃ c, 0 < c ∧ ∀ (k : ℕ), 3 ≤ k → ∃ C, ∀ᶠ (l : ℕ) in Filter.atTop, ↑R(k, l + 1) ≤ (1 + C * ↑l ^ (-c / ↑k ^ 2)) * ↑R(k, l)

SolvedStatement only, no proof