Let $t \geq 1$ and let $d_{t}$ be the density of the set of integers $n \in N$ for which $t$ can be represented as the sum of distinct divisors of $n$ .Do there exist constants $c_{1}, c_{2} > 0$ such that $d_{t} \sim \frac{c _{1}}{( lo g t ) ^{c_{2}}}$ as $t \to \infty$ ?

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

As far as I can find in the literature, this is **open**.

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · solved (literature)

theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ),
    ∀ᶠ t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧
    1 / Real.log t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log t ^ c₄

formal-conjectures/859.lean ↗

status

open

evidence

formal

status

Search Vela