Erdős problem 955
If has density then must also have density .
Sources
FormalConjectures/ErdosProblems/
955.lean
Retained formal statement
Pollack [Po14b] has shown that this is true if is the set of primes.
{x | Nat.Prime (Erdos955.s x)}.HasDensity 0SolvedStatement only, no proof