Ben Green's Open Problem 45

Can we pick residue classes $a_p \pmod{p}$, one for each prime $p \leq N$, such that every integer $\leq N$ lies in at least 10 of them?

References:

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

This file points to the canonical formalization in FormalConjectures.ErdosProblems.«689».