An Exponential Improvement for Diagonal Ramsey

The (diagonal) Ramsey number $R(k)$ denotes the minimum size of a complete graph such that every red-blue colouring of its edges contains a monochromatic subgraph of size $k$. In 1935, Erdős and Szekeres found an upper bound, proving that $R(k)\le 4^k$. Somewhat later, a lower bound of $\sqrt{2}^k$ was established. In subsequent improvements to the upper bound, the base of the exponent stubbornly remained at 4 until March 2023, when Campos et al. sensationally showed that $R(k)\le (4-\epsilon)^k$ for a particular small positive $\epsilon$. The Isabelle/HOL formalisation of the result presented here is largely independent of the prior formalisation (in Lean) by Bhavik Mehta.