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
Gowers [Go01] has proved W(k) \leq 2^{2^{2^{2^{2^{k+9}}}}.
∀ (k : ℕ), Erdos138.W k ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ (k + 9)SolvedStatement only, no proof