Abstract
This article is a formalisation of a proof of the Hales–Jewett theorem presented in the textbook Ramsey Theory by Graham et al.
The Hales–Jewett theorem is a result in Ramsey Theory which states that, for any non-negative integers $r$ and $t$, there exists a minimal dimension $N$, such that any $r$-coloured $N'$-dimensional cube over $t$ elements (with $N' \geq N$) contains a monochromatic line. This theorem generalises Van der Waerden's Theorem, which has already been formalised in another AFP entry.