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
Erdős [Er80] seems to credit Mirsky and Newman with the result that , but gives no reference.
∀ (m : ℕ), 1 ≤ m → ∀ (S : Finset ℕ) (a : ℕ → ℤ), (∀ n ∈ S, m < n) → (∀ n ∈ S, ∀ n' ∈ S, n ≠ n' → ¬∃ x, x ≡ a n [ZMOD ↑n] ∧ x ≡ a n' [ZMOD ↑n']) → ∑ n ∈ S, (↑n)⁻¹ < 1SolvedStatement only, no proof