theorem
erdos_412 :
(∀ m ≥ 2, ∀ n ≥ 2, ∃ (i : ℕ) (j : ℕ), (⇑(ArithmeticFunction.sigma 1))^[i] m = (⇑(ArithmeticFunction.sigma 1))^[j] n) ↔ sorry
Let $σ_1(n)=σ(n)$, the sum of divisors function, and $σ_k(n) = σ(σ_{k−1}(n))$. Is it true that, for every $m, n ≥ 2$, there exist some $i, j$ such that $σ_i(m) = σ_j(n)$?