Erdős problem 1014 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

2 retained statements2415f78e850a

Open selected source

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

Sources

Search problems.science