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’ >= N) contains a monochromatic line. This theorem generalises Van der Waerden’s Theorem, which has already been formalised in another AFP entry.

BibTeX

@article{Hales_Jewett-AFP,
  author  = {Ujkan Sulejmani and Manuel Eberl and Katharina Kreuzer},
  title   = {The {H}ales–{J}ewett Theorem},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2022},
  note    = {\url{https://isa-afp.org/entries/Hales_Jewett.html},
            Formal proof development},
  ISSN    = {2150-914x},
}