### 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$.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Van_der_Waerden

- Digits
- Van_der_Waerden

## Cite

×

Van_der_Waerden-AFP

    @article{Van_der_Waerden-AFP,
      author  = {Katharina Kreuzer and Manuel Eberl},
      title   = {Van der Waerden's Theorem},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Van_der_Waerden.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Jun 23, 2021 : Isabelle2021