Finite Ramsey theorem for graphs

← All problems

finite_graph_ramsey_theorem

Submitter: Kim Morrison.

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 := ⊢ ∀ (r s : ℕ), 2 ≤ r → 2 ≤ s → ∃ n, ∀ (G : SimpleGraph (Fin n)), ¬G.CliqueFree r ∨ ¬Gᶜ.CliqueFree s All goals completed! 🐙

Solved by

• @rkirov with Claude Opus 4.7 on Apr 30, 2026 (proof)

• @kim-em with Aristotle (Harmonic) on May 1, 2026 (proof)

• @rkirov with Claude Opus 4.7 (1M context) on May 2, 2026 (proof)

• @sqrt-of-2 with GPT-5.5 on May 7, 2026 (proof)

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 8, 2026

• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 13, 2026 (proof)

• @machinelearning2014 with EVO on May 20, 2026 (proof)

• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026