An Exponential Improvement for Diagonal Ramsey

Lawrence C. Paulson 📧

September 2, 2024

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

BSD 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