Erdős problem 138
If is the least such that every two-colouring of contains a monochromatic -term arithmetic progression, must ?
Sources
FormalConjectures/ErdosProblems/
138.lean
Retained formal statement
In [Er80] Erdős asks whether
True ↔ Filter.Tendsto (fun k => ↑(Erdos138.W k) ^ (1 / ↑k)) Filter.atTop Filter.atTopOpenStatement only, no proof