Erdős problem 859
The density of the divisor sum set is asymptotically equivalent to .
Sources
FormalConjectures/ErdosProblems/
859.lean
Retained formal statement
A case where we can easily calculate the density of DivisorSumSet t is that of t=0.
Erdos859.DivisorSumSet 0 = Set.univTextbookStatement only, no proof