Erdős problem 1190
Let where the maximum is taken over all finite sequences for which there exist congruences such that no integer satisfies two such congruences.
Sources
FormalConjectures/ErdosProblems/
1190.lean
Retained formal statement
He could not even decide whether as .
Filter.Tendsto Erdos1190.eps Filter.atTop (nhds 0)SolvedStatement only, no proof