The Hales–Jewett Theorem

Ujkan Sulejmani 📧, Manuel Eberl 📧 and Katharina Kreuzer 📧

September 2, 2022


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.

BSD License


Theories of Hales_Jewett