Number theory · Last catalog review 26 Jul 2026

Erdős Problem 859

The density of the divisor sum set is asymptotically equivalent to

c_1 / \log(t)^{c_2}

References

erdosproblems.com/859

Published 24 Jun 2026Never attempted

Formal statement

Lean type

∃ c₁ > 0,
  ∃ c₂ > 0,
    ∃ d,
      (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧
        Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂

What you must prove

import FormalConjectures.ErdosProblems.«859»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos859.erdos_859" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/859.lean

Source type SHA-256: sha256:8c497b4f2a8504f2d06c6ffd6524c4773fa037d7c99a539a3efbd9809e173f99
Task id: fc-e923379e-erdos859-erdos-859-8e70ce7ef3-formalized-v1
Task commitment: sha256:43c2d93a19938849f1d84bb8e21a5ad75b8c84376bcbbd0152f91d405f1d3df2

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.