Erdős Problem 410

Reference: erdosproblems.com/410

theorem erdos_410 : (∀ n > 1, Filter.Tendsto (fun (k : ℕ) => ↑((⇑(ArithmeticFunction.sigma 1))^[k] n) ^ (1 / ↑k)) Filter.atTop Filter.atTop) ↔ sorry

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