Skip to content

Erdős problem 859

The density of the divisor sum set is asymptotically equivalent to c1/log(t)c2c_1 / \log(t)^{c_2}.

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

859.lean

Retained formal statement3 of 4

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.

FormalConjectures/ErdosProblems/859.leanErdos859.erdos_859.variants.positive_density1 lineExact file
∀ (t : ℕ), (Erdos859.DivisorSumSet t).HasPosDensity
TextbookStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page