Erdős problem 138

If $W(k)$ is the least $N$ such that every two-colouring of $\{1, \dots, N\}$ contains a monochromatic $k$ -term arithmetic progression, must $W(k+1) - W(k) \to \infty$ ?

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

138.lean

Retained formal statement1 of 9

In [Er80] Erdős asks whether $\lim_{k \to \infty} (W(k))^{1/k} = \infty$

FormalConjectures/ErdosProblems/138.leanErdos138.erdos_1381 lineExact file

1True ↔ Filter.Tendsto (fun k => ↑(Erdos138.W k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

OpenStatement only, no proof