Erdős Problem 1030

Conjecture 1030 · Erdős

Let $R(k,l)$ be the usual Ramsey number: the smallest $n$ such that if the edges of $K_n$ are coloured red and blue then there exists either a red $K_k$ or a blue $K_l$ .

Prove the existence of some $c>0$ such that $\lim_{k\to \infty}\frac{R(k+1,k)}{R(k,k)}> 1+c.$

A problem of Erdős and Sós.

Formal statement · Lean 4.lean

theorem erdos_1030 :
    ∃ c > (0 : ℝ), ∃ L : ℝ,
      Tendsto (fun k : ℕ ↦
        (SimpleGraph.classicalRamsey (k + 1) k : ℝ) /
          (SimpleGraph.classicalRamsey k k : ℝ)) atTop (nhds L) ∧
      L > 1 + c := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗