The Hales-Jewett Theorem

Ujkan Sulejmani, Manuel Eberl, Katharina Kreuzer
Archive of Formal Proofs 2022.

pdf AFP entry

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},
}