Van der Waerden's Theorem

 

Title: Van der Waerden's Theorem
Authors: Katharina Kreuzer and Manuel Eberl
Submission date: 2021-06-22
Abstract: This article formalises the proof of Van der Waerden's Theorem from Ramsey theory. Van der Waerden's Theorem states that for integers $k$ and $l$ there exists a number $N$ which guarantees that if an integer interval of length at least $N$ is coloured with $k$ colours, there will always be an arithmetic progression of length $l$ of the same colour in said interval. The proof goes along the lines of \cite{Swan}. The smallest number $N_{k,l}$ fulfilling Van der Waerden's Theorem is then called the Van der Waerden Number. Finding the Van der Waerden Number is still an open problem for most values of $k$ and $l$.
BibTeX:
@article{Van_der_Waerden-AFP,
  author  = {Katharina Kreuzer and Manuel Eberl},
  title   = {Van der Waerden's Theorem},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/Van_der_Waerden.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License