Erdős problem 859
The density of the divisor sum set is asymptotically equivalent to .
Sources
FormalConjectures/ErdosProblems/
859.lean
Retained formal statement
An easy sanity check is to prove that for every natural number t the density dₜ is a positive number. Hint: investigate some multiplicative structure of DivisorSumSet t.
∀ (t : ℕ), (Erdos859.DivisorSumSet t).HasPosDensityTextbookStatement only, no proof