Catalog.Sparsity.Ramsey

Theorem

Let \(a, b \in \mathbb{N}\). Then there exists a number \(R(a, b)\) such that for every coloring of the edges of a complete graph on \(R(a, b)\) vertices with colors red and blue we will either find a clique on \(a\) vertices whose edges are all blue or a clique on \(b\) vertices whose edges are all red.

Review notes

The source states Ramsey’s theorem as: for every \(a, b \in \mathbb{N}\), there exists \(R(a,b)\) such that every \(2\)-coloring of the edges of \(K_{R(a,b)}\) yields a monochromatic clique. We reformulate this using Mathlib’s SimpleGraph.CliqueFree:

\(\lnot\)G.CliqueFree a means \(G\) contains a clique of size \(a\) (a “blue” monochromatic clique).
\(\lnot\)G^c.CliqueFree b means the complement \(G^c\) contains a clique of size \(b\), i.e., \(G\) contains an independent set of size \(b\) (a “red” monochromatic clique).

This is equivalent to the source statement: a \(2\)-coloring of \(K_N\) is the same as a graph \(G\) on \(N\) vertices (blue edges are edges of \(G\), red edges are non-edges). The Lean formulation quantifies over all types V with Fintype.card V \(\geq\) N, which is equivalent to the source’s “complete graph on \(R(a,b)\) vertices.”

Mathlib has no Ramsey theory. The proof (Phase 4) will be by induction on \(a + b\), following the source.

Catalog/Sparsity/Ramsey/Contract.lean (full)

1	import Mathlib.Combinatorics.SimpleGraph.Clique
2
3	namespace Catalog.Sparsity.Ramsey
4
5	/-- Ramsey's theorem (two colors): for any `a b : ℕ` there exists `N` such that
6	every graph on at least `N` vertices either contains a clique of size `a` or
7	an independent set of size `b`. (Theorem 3.7) -/
8	axiom ramsey (a b : ℕ) : ∃ N : ℕ,
9	∀ {V : Type} [DecidableEq V] [Fintype V] (G : SimpleGraph V)
10	[DecidableRel G.Adj],
11	N ≤ Fintype.card V → ¬G.CliqueFree a ∨ ¬Gᶜ.CliqueFree b
12
13	end Catalog.Sparsity.Ramsey
14

Used By

Proof