FormalConjectures/ErdosProblems/410.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 410

Reference: erdosproblems.com/410

Imports (1)
  1. theorem Erdos410.erdos_410 Let $σ_1(n) = σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k-1}(n))$ sorry line 43 source

    Source documentation

    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).

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GT.gt, OfNat.ofNat, Filter.Tendsto, Real, HPow.hPow, Nat.iterate, ArithmeticFunction, ArithmeticFunction.sigma, HDiv.hDiv, Filter.atTop

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_410 : answer(sorry) ↔ ∀ n > 1,
    Tendsto (fun k : ℕ ↦ ((sigma 1)^[k] n : ℝ) ^ (1 / (k : ℝ))) atTop atTop := by
…