# Superexponential van der Waerden numbers

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Quantitative Superexponential Bounds for van der Waerden Numbers](../../preprints/Quantitative-Superexponential-Bounds-for-van-der-Waerden-Numbers-September-23-2026/paper.pdf)

## Scope

Let $W(r,k)$ be the least interval length forcing a monochromatic $k$-term arithmetic progression in every coloring with at most $r$ colors. The formalized result gives an absolute threshold $K$ such that $W(r,k)>k^{k\lfloor\log_2 r\rfloor/100000}$ for all $k\ge K$ and $r\ge2$. It also establishes the associated growth limits, finiteness, and boundary values. The sharper intermediate estimates used in the paper are not part of the described formalization.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform van der Waerden lower bound | [QuantitativeVanDerWaerden.lean](../ComparatorChallenges/QuantitativeVanDerWaerden.lean) |