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:

• Yamaan Attwa
• Aldo Kiem
• Olivia Röhrig
• Christoph Spiegel

Mathlib PRs

This project has contributed 3 merged PRs to Mathlib.

Contribution	Status & PR
Probability Classical scope cleanup Removed unnecessary 'open scoped Classical' from uniformOfFintype theorems, fixing hard-to-debug errors from implicit classical usage. Mathlib.Probability.Distributions.Uniform	✓ Cleaned #24074 2025-04-21
SimpleGraph abbrev refactor Refactored completeGraph and emptyGraph to be abbreviations for the lattice operations ⊤ and ⊥ on SimpleGraph. Mathlib.Combinatorics.SimpleGraph.Basic	✓ Cleaned #23838 2025-05-10
Integrability of shifted power function Proves that (fun t : ℝ ↦ (t + m) ^ a) is integrable on (c, ∞) for 0 ≤... Mathlib.Analysis.SpecialFunctions.Integrals	✓ Cleaned #25045 2025-05-30

Legend: ○ Tentative · ◐ Branch · → Ready · ⟳ Submitted · ✓ Merged · ✓ Cleaned