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
Let . What is the largest such that there are with a non-empty arithmetic progression for all ?
Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos272.maxArithInterCard N)) sorryOpenStatement only, no proof