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
The work of de la Bretèche, Ford, and Vandehey [BFV13] implies where . The lower bound is implicit in their construction.
∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps mSolvedStatement only, no proof