The purpose of this repository is to hold a LEAN4 formalization of Upper bounds for multicolour Ramsey numbers by Balister et al. (2024). The following people is an alphabetical list of contributors: