# mathlibdocumentation

combinatorics.hales_jewett

# The Hales-Jewett theorem #

We prove the Hales-Jewett theorem and deduce Van der Waerden's theorem as a corollary.

The Hales-Jewett theorem is a result in Ramsey theory dealing with combinatorial lines. Given an 'alphabet' α : Type* and a b : α, an example of a combinatorial line in α^5 is { (a, x, x, b, x) | x : α }. See combinatorics.line for a precise general definition. The Hales-Jewett theorem states that for any fixed finite types α and κ, there exists a (potentially huge) finite type ι such that whenever ι → α is κ-colored (i.e. for any coloring C : (ι → α) → κ), there exists a monochromatic line. We prove the Hales-Jewett theorem using the idea of color focusing and a product argument. See the proof of combinatorics.line.exists_mono_in_high_dimension' for details.

The version of Van der Waerden's theorem in this file states that whenever a commutative monoid M is finitely colored and S is a finite subset, there exists a monochromatic homothetic copy of S. This follows from the Hales-Jewett theorem by considering the map (ι → S) → M sending v to ∑ i : ι, v i, which sends a combinatorial line to a homothetic copy of S.

## Main results #

• combinatorics.line.exists_mono_in_high_dimension: the Hales-Jewett theorem.
• combinatorics.exists_mono_homothetic_copy: a generalization of Van der Waerden's theorem.

## Implementation details #

For convenience, we work directly with finite types instead of natural numbers. That is, we write α, ι, κ for (finite) types where one might traditionally use natural numbers n, H, c. This allows us to work directly with α, option α, (ι → α) → κ, and ι ⊕ ι' instead of fin n, fin (n+1), fin (c^(n^H)), and fin (H + H').

## Todo #

• Prove a finitary version of Van der Waerden's theorem (either by compactness or by modifying the current proof).

• One could reformulate the proof of Hales-Jewett to give explicit upper bounds on the number of coordinates needed.

## Tags #

combinatorial line, Ramsey theory, arithmetic progession