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) / 2 ^ k) Filter.atTop Filter.atTopOpenStatement only, no proof