Erdős Problem 159

Conjecture 159 · Erdős

There exists some constant $c>0$ such that $R(C_4,K_n) \ll n^{2-c}.$

The prize of $100 is offered in [Er78] for a proof or disproof.

This problem is #17 in Ramsey Theory in the graphs problem collection.

Formal statement · Lean 4.lean

theorem erdos_159 :
    ∃ (c : ℝ) (_ : 0 < c) (C : ℝ),
      ∀ (n : ℕ), 1 ≤ n →
        (SimpleGraph.graphRamsey (SimpleGraph.cycleGraph 4)
          (SimpleGraph.completeGraph (Fin n)) : ℝ) ≤ C * (n : ℝ) ^ (2 - c) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗