1 Introduction

This blueprint formalizes the proof from [ 1 ] of an exponential improvement to the classical Erdős-Szekeres upper bound for multicolor Ramsey numbers.

The \(r\)-color Ramsey number \(R_r(k)\) is the minimum \(n\) such that every \(r\)-coloring of the edges of the complete graph \(K_n\) contains a monochromatic clique \(K_k\). Ramsey [ 3 ] proved in 1930 that these numbers are finite, and Erdős and Szekeres [ 2 ] showed in 1935 that \(R_r(k) \le r^{rk}\). For over 85 years, no improvement was known for the case \(r \ge 3\).

The main result of this formalization establishes the first exponential improvement over the Erdős-Szekeres bound for all \(r \ge 2\):

Theorem 1

Theorem 1.1

For each \(r \ge 2\), there exists \(\delta = \delta (r) {\gt} 0\) such that

\begin{equation*} R_r(k) \le e^{-\delta k} r^{rk} \end{equation*}

for all sufficiently large \(k \in \mathbb {N}\).

The proof introduces a new “select and boost” algorithm that iteratively finds large monochromatic substructures using a geometric lemma based on moment inequalities.