Erdős Problem 1029

Conjecture 1029 · Erdős

If $R(k)$ is the Ramsey number for $K_k$ , the minimal $n$ such that every $2$ -colouring of the edges of $K_n$ contains a monochromatic copy of $K_k$ , then $\frac{R(k)}{k2^{k/2}}\to \infty.$

In [Er93] Erdős offers $100 for a proof of this and$ 1000 for a disproof, but says 'this last offer is to some extent phoney: I am sure that this is true (but I have been wrong before).'

Formal statement · Lean 4.lean

theorem erdos_1029 :
    Tendsto (fun k : ℕ ↦ (SimpleGraph.diagonalRamsey k : ℝ) /
      ((k : ℝ) * (2 : ℝ) ^ ((k : ℝ) / 2))) atTop atTop := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗