therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 1060: I

The conjecture is about the function f(n)f(n) which counts the number of solutions to kσ(k)=nk\sigma(k)=n, where σ(k)\sigma(k) is the sum of divisors of kk. The first bound is that f(n)f(n) grows slower than any power of n(1log⁡log⁡n)n^(\frac{1}{\log\log n}). The second bound i...

Number theoryAMS 11

Mathematical statement

The conjecture is about the function f(n)f(n) which counts the number of solutions to kσ(k)=nk\sigma(k)=n, where σ(k)\sigma(k) is the sum of divisors of kk. The first bound is that f(n)f(n) grows slower than any power of n(1log⁡log⁡n)n^(\frac{1}{\log\log n}). The second bound is that f(n)f(n) is at most a power of log⁡n\log n.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_1060.parts.i

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_1060.parts.i :    ∃ h : ℕ → ℝ,      h =o[atTop] (fun n ↦ 1 / log (log n)) ∧ ∀ᶠ n in atTop, #{k ≤ n | k * σ 1 k = n} ≤ (n : ℝ) ^ h n := by sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationerdosproblems.com/1060background