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 showed that the maximal is equal to
(fun N => ↑(Erdos272.maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun N => ↑N ^ (5 / 3) * Real.log ↑N ^ 3SolvedStatement only, no proof