### Abstract

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.

### License

### Topics

### Related publications

- Campos, M., Griffiths, S., Morris, R., & Sahasrabudhe, J. (2023).
*An exponential improvement for diagonal Ramsey*(Version 1). arXiv. https://doi.org/10.48550/ARXIV.2303.09521

### Session Diagonal_Ramsey

- General_Extras
- Neighbours
- Book
- Big_Blue_Steps
- Red_Steps
- Bounding_Y
- Bounding_X
- Zigzag
- Far_From_Diagonal
- Closer_To_Diagonal
- From_Diagonal
- The_Proof