Ramsey numbers

The (graph) Ramsey number $R(k,\ell)$ is the least natural number $n$ such that every simple graph on $n$ vertices contains either a clique of size $k$ or an independent set of size $\ell$ (equivalently, the complement graph contains a clique of size $\ell$).

We formalize the classical open problem of determining $R(5,5)$, together with the currently best known bounds $43 \le R(5,5) \le 46$.

Note: the diagonal Ramsey number $R(n,n)$ can also be formulated in terms of 2-colorings of $2$-subsets, as Combinatorics.hypergraphRamsey 2 n (see FormalConjecturesForMathlib/Combinatorics/Ramsey.lean).

References:

• Wikipedia: Ramsey number
• [Rad] S. P. Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1. (Updated periodically.) https://www.combinatorics.org/ojs/index.php/eljc/article/view/DS1
• [Exoo89] G. Exoo, A lower bound for $R(5,5)$, Journal of Graph Theory 13 (1989), 97–98. DOI: 10.1002/jgt.3190130113
• [AM24] V. Angeltveit and B. McKay, $R(5,5) \le 46$, arXiv:2409.15709 (2024).
• OEIS A212954
• MathWorld: Ramsey Number

def RamseyNumbers.IsGraphRamsey (n k l : ℕ) : Prop

IsGraphRamsey n k l means that for every simple graph G on n vertices, either

• G contains a clique of size k, or
• the complement graph Gᶜ contains a clique of size l (equivalently, G contains an independent set of size l).

Equations

• RamseyNumbers.IsGraphRamsey n k l = ∀ (G : SimpleGraph (Fin n)), ¬(G.CliqueFree k ∧ Gᶜ.CliqueFree l)

theorem RamseyNumbers.IsGraphRamsey.succ (n k l : ℕ) : IsGraphRamsey n k l → IsGraphRamsey (n + 1) k l

Monotonicity in the number of vertices.

theorem RamseyNumbers.IsGraphRamsey.symm (n k l : ℕ) : IsGraphRamsey n k l ↔ IsGraphRamsey n l k

Symmetry in the clique / independent set sizes.

noncomputable def RamseyNumbers.graphRamseyNumber (k l : ℕ) : ℕ

The (graph) Ramsey number R(k,l) is the least natural number n such that IsGraphRamsey n k l holds.

Equations

• R(k, l) = sInf {n : ℕ | RamseyNumbers.IsGraphRamsey n k l}

def RamseyNumbers.«termR(_,_)» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem RamseyNumbers.ramsey_number_five_five : R(5, 5) = sorry

The open problem: determine the Ramsey number $R(5,5)$.

It is known that $43 \le R(5,5) \le 46$.

theorem RamseyNumbers.ramsey_number_five_five_lower_bound : ∃ (G : SimpleGraph (Fin 42)), G.CliqueFree 5 ∧ Gᶜ.CliqueFree 5

Lower bound $43 \le R(5,5)$, equivalently: there exists a graph on $42$ vertices with no $5$-clique and no independent set of size $5$.

theorem RamseyNumbers.ramsey_number_five_five_upper_bound : IsGraphRamsey 46 5 5

Upper bound $R(5,5) \le 46$, i.e. every graph on $46$ vertices contains a $5$-clique or an independent set of size $5$.