Van der Waerden numbers: exact values and bounds

### What is the conjecture

The **Van der Waerden number** $W(r, k)$ is the smallest positive integer $n$ such that for every partition of the set $\{1, 2, \ldots, n\}$ into $r$ disjoint subsets, at least one subset contains an arithmetic progression of length $k$.

The core open problem is to determine exact values of $W(r, k)$ for arbitrary pairs $(r, k)$. Known exact values are extremely rare: only the pairs $(2, 1), (2, 2), (2, 3), (2, 4), (2, 5), (2, 6), (3, 3), (4, 3), (5, 3), (6, 3), (2, 8), (3, 4)$ have been computed exactly. Computing even the next value remains an open computational challenge. Related open problems include improving upper and lower bounds for $W(r, k)$ and determining whether the mixed van der Waerden numbers are concave.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- - [Wikipedia: Van der Waerden number](https://en.wikipedia.org/wiki/Van_der_Waerden_number)
- [Wolfram MathWorld: Van der Waerden Numbers](https://mathworld.wolfram.com/vanderWaerdenNumber.html)
- [Open Problem Garden: Concavity of van der Waerden numbers](http://www.openproblemgarden.org/op/concavity_of_van_der_waerden_numbers)
- [Samvar, H. "Van der Waerden's Theorem", 2022](https://simonrs.com/eulercircle/irpw2022/samvar-vdwaerden-paper.pdf)
- [Grier, D. "On the Cyclic Van der Waerden Numbers"](https://danielgrier.com/documents/cyclic_waerden.pdf)

### Prerequisites needed

**Formalizability Rating:** 1/5 (0 is best) (as of 2026-02-14)

Building blocks (1-3; from search results):
- `Set.IsAPOfLengthWith`, `List.IsAPOfLengthWith` (arithmetic progression definitions available in FormalConjecturesForMathlib/Combinatorics/AP/Basic.lean)
- Finset partitions and colorings (standard in Mathlib)
- Finite set cardinality and ordering (Mathlib.Data.Finset, Mathlib.Order)

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition/API for "partitioning a finset into r disjoint subsets" with convenient notation for the coloring argument
- Library lemma connecting arithmetic progression membership to color classes in a partition

Rating justification (1-2 sentences): The statement can be written immediately using existing Mathlib definitions for finite sets, partitions, and the arithmetic progression helpers available in the repo. Only minor auxiliary definitions for clean API design would be needed; the core mathematical objects are all present.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-05
* ams-11

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)