Erdős Problem 689 #
Reference: erdosproblems.com/689
theorem
Erdos689.erdos_689 :
(∀ n ≥ 3,
∃ (a : ℕ → ℕ),
∀ m ∈ Finset.Icc 1 n, 2 ≤ (Finset.filter (fun (p : ℕ) => Nat.Prime p ∧ a p ≡ m [MOD p]) (Finset.Icc 1 n)).card) ↔ sorry
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)?