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
When is prime Berlekamp [Be68] has proved .
∀ (p : ℕ), Nat.Prime p → p * 2 ^ p ≤ Erdos138.W (p + 1)SolvedStatement only, no proof