Van der Waerden numbers: exact values and bounds

[franzhusch]

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
• Wolfram MathWorld: Van der Waerden Numbers
• Open Problem Garden: Concavity of van der Waerden numbers
• Samvar, H. "Van der Waerden's Theorem", 2022
• Grier, D. "On the Cyclic Van der Waerden Numbers"

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

• ams-05
• ams-11

Choose either option

• I plan on adding this conjecture to the repository
• 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

Feedback on mistakes/hallucinations: link

[Rafiaminhaj]

Hello @franzhusch ,

I am interested in working on this issue as part of my OSCG 2026 open source contribution journey.

I have reviewed the conjecture description and the mentioned prerequisites, including arithmetic progression definitions and finset partition concepts in Mathlib. I would like to contribute by formalizing the Van der Waerden number conjecture and implementing the required auxiliary definitions for finset partitions and coloring arguments.

I will start by exploring the existing combinatorics and number theory modules in the repository and then work on adding a clean and structured formal statement of the conjecture.

Please let me know if you have any specific guidance, preferred structure, or references I should follow before starting.

Thank you!

[franzhusch]

Hi Rafia,

Great that you chose to contribute to the Formal Conjectures Repo :). For preferred structure and general best practices, you can essentially look at the general information in the README.md. For more specific information, you can view other files in the repository as an example or look at the AGENTS.md in #2182.

[jeangud]

Very cool @Rafiaminhaj !

FYI #2005 could be useful for some of the building blocks, and you might have some complementary ideas on the implementation as well.

[franzhusch]

@jeangud doesnt your PR cover the complete conjectures(s) as described here in the issue? It might make more sense that you add a duplicate file in the Wikipedia Folder in #2005 and we just close this issue when your PR has gone through.

[franzhusch]

If you want @Rafiaminhaj, to avoid having effort wasted, work on another good first issue such as #2247 or (maybe a bit harder) #2248

[jeangud]

@jeangud doesnt your PR cover the complete conjectures(s) as described here in the issue? It might make more sense that you add a duplicate file in the Wikipedia Folder in #2005 and we just close this issue when your PR has gone through.

@franzhusch
Perhaps not exactly, #2005 covers the 2-colour case only, and for asymmetric APs ($k$ for red AP, $r$ for blue AP). It looks like @Rafiaminhaj's focus is on the more general $r$-color case and symmetric (any color) $k$-length AP (different meaning for $r$ and $k$). Also, I have not looked at the concavity conjecture mentioned above.

Happy to re-use #2005 in the Wikipedia folder if you think they're equivalent though (something like 81.lean). Let me know 👍

[franzhusch]

Ah good point, I didnt read the PR exactly enough. Then it probably makes sense to only %type_of the relevant theorems / conjectures (about the values) from #2005 and the rest will be new conjectures, such as concavity and what else is in the Wikipedia Page.