Number theory
Approved
The natural density of integers whose distinct divisors can sum to a prescribed target exists, but it does not have the proposed positive-constant logarithmic-power asymptotic.
Submitted by JenW1N
The PDF is a working mathematical exposition. Lean verification applies to the formal source, not the prose.
Formal statement
Proof target
import Mathlib
import FormalConjectures.ErdosProblems.«859»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos859.erdos_859" := by
sorry
end Bounty
Original conjecture (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₂Original conjecture source: FormalConjectures/ErdosProblems/859.lean
References
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.
Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.
1 piece · 7 lemmas
Individual lemmas, special cases and supporting work, shown in their original scope.
1 Sept 2026
The divisor-sum set has a density, and it is positive
5FqLp5…FfZZiK · 7 lemmas
conjectures-tasks
The pinned statement, the Lean challenge file and the exact bundle you build against.
versions/fc-v2-erdos859-erdos-859-44b450dd332232ed1ce2cba9-formalized →
conjectures-contribution
Every published piece for this problem, with its Lean source and its signed record.
contributions/erdos-859 →