ErdosProblems · research open · AMS 11

unsolvedsorry — nobody on it

Erdős Problem 859

Conjecture 859 · Erdős

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

Formal statement · Lean 4.lean
theorem erdos_859 :
    ∃ c₁ > 0, ∃ c₂ > (0 : ℝ), ∃ d : ℕ → ℝ, (∀ t > 0, (DivisorSumSet t).HasDensity (d t)) ∧
      (fun (t : ℕ) ↦ d t) ~[atTop] (fun t ↦ c₁ / Real.log t ^ c₂) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗