Erdős problem 955
If has density then must also have density .
Sources
FormalConjectures/ErdosProblems/
955.lean
Retained formal statement
Troupe [Tr15] has shown that this is true if is the set of integers with unusually many prime factors.
∀ ε > 0, {x | (1 + ε) * Real.log (Real.log ↑(Erdos955.s x)) < ↑(ArithmeticFunction.cardDistinctFactors (Erdos955.s x))}.HasDensity 0SolvedStatement only, no proof