Let the van der Waerden number $W (k)$ be such that whenever $N \geq W (k)$ and ${1, \dots, N}$ is $2$ -coloured there must exist a monochromatic $k$ -term arithmetic progression. Improve the bounds for $W (k)$ - for example, prove that $W (k)^{1/ k} \to \infty$ .

Worked, still open.

additive combinatorics · open · prize $500 · formalized (Lean) · 0 attempts

machinery: additive-combinatorics,van-der-Waerden-number,Szemeredi-regularity,hypergraph-container,probabilistic-coloring,arithmetic-progressions,graph-coloring

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

alphaproof · AlphaProof Nexus (DeepMind) · machine-verified (Lean)

Machine-verified Lean proof (kernel-checkable, sorry-free).

Lean proof ↗

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let (W(k)=W(2,k)) be the least $N$ such that **every** red/blue colouring of ({1,\dots,N}) contains a monochromatic $k$-term arithmetic progression.

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · solved (literature)

theorem monoAP_guarantee_set_nonempty (r k) : (monoAP_guarantee_set r k).Nonempty

formal-conjectures/138.lean ↗

Kernel-checked proof; human-attested statement.

variant — reviewer:will-blair erdos_138.variants.difference.lean

oeis

A005346 — Van der Waerden numbers W(2,n).1,3,9,35,178,1132

links

#169Let

k \geq 3

and

f (k)

be the supremum of

\sum_{n \in A} \frac{1}{n}

A

ranges over all sets of positive integers which do not contain a

k

-term arithmetic progression. Estimate

f (k)

. Is

k \to \infty lim \frac{f ( k )}{lo g W ( k )} = \infty

where

W (k)

is the van der Waerden number?A005346

status