Finite Ramsey theorem for graphs | Lean AI formalization leaderboard

Problem statement

Notes: States finite Ramsey existence for red/blue edge colourings of complete graphs, encoded by a graph and its complement.

Source: Classical theorem in Ramsey theory.

Informal solution: Show that for every r and s there is an n such that every graph on n vertices contains either a clique of size r or an independent set of size s.

theorem declaration uses `sorry`finite_graph_ramsey_theorem :
    ∀ r s : ℕ, 2 ≤ r → 2 ≤ s → ∃ n : ℕ, ∀ G : SimpleGraph (Fin n), ¬ G.CliqueFree r ∨ ¬ Gᶜ.CliqueFree s := by⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s
  sorryAll goals completed! 🐙