Erdős Problem 689

Reference: erdosproblems.com/689

theorem Erdos689.erdos_689 : (∀ᶠ (n : ℕ) in Filter.atTop, ∃ (a : ℕ → ℕ), ∀ m ∈ Finset.Icc 1 n, 2 ≤ {p ∈ Finset.Icc 1 n | Nat.Prime p ∧ a p ≡ m [MOD p]}.card) ↔ sorry

Let n be sufficiently large. Is there some choice of congruence class a_p for all primes 2 ≤ p ≤ n such that every integer in [1,n] satisfies at least two of the congruences ≡ a_p (mod p)?