Ben Green's Open Problem 45

Can we pick residue classes $a_p(mod p)$, one for each prime p ⩽ N, such that every integer ⩽ N lies in at least 10 of them?

References:

• Ben Green's Open Problem 45
• erdosproblems.com/689

theorem Green45.green_45 : sorry ↔ ∀ᶠ (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