Erdős problem 142
Prove an asymptotic formula for , the largest possible size of a subset of that does not contain any non-trivial -term arithmetic progression.
Sources
FormalConjectures/ErdosProblems/
142.lean
Retained formal statement
Prove an asymptotic formula for , the largest possible size of a subset of that does not contain any non-trivial -term arithmetic progression.
(fun N => ↑(Erdos142.r 3 N)) =Θ[Filter.atTop] sorryOpenStatement only, no proof