Number theory

Erdős 859

The density of the divisor sum set is asymptotically equivalent to

c_1 / \log(t)^{c_2}

References

erdosproblems.com/859

No one has attempted this yet.

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-379fc029-erdos859-erdos-859-f1996443f0-formalized-v1
Task commitment: sha256:108d7a1c681cef0fc2660e40445006bee3d08acdbb37a8b6cf0923b5c5b6aaed

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.