Source labels openChecked July 26, 2026

Erdős Problem 410

Let $σ_1(n) = σ(n)$ , the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$ .

Mathematical statement

Let $σ_1(n) = σ(n)$ , the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$ .

Is it true that $\lim_{k → ∞} σ_k(n)^{\frac 1 k} = ∞$ ?

This is problem (iii) from Erdos, Granville, Pomerance, Spiro "On the normal behavior of the iterates of some arithmetical functions" (page 169 of the book "Analytic Number Theory", 1990).

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_410

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_410 : answer(sorry) ↔ ∀ n > 1,    Tendsto (fun k : ℕ ↦ ((sigma 1)^[k] n : ℝ) ^ (1 / (k : ℝ))) atTop atTop := 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 sourceformalization erdosproblems.com/410background