Erdős problem 689

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)`?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

689.lean

Retained formal statement1 of 1

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)?

FormalConjectures/ErdosProblems/689.leanErdos689.erdos_6892 linesExact file

1sorry ↔2  ∀ᶠ (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

OpenStatement only, no proof