Erdős problem 272
Let . What is the largest such that there are with a non-empty arithmetic progression for all ?
Sources
FormalConjectures/ErdosProblems/
272.lean
Retained formal statement
Szabo asks whether the maximal is given by
(fun N => ↑(Erdos272.maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun N => ↑NOpenStatement only, no proof