Erdős Problem 414

Reference: erdosproblems.com/414

def Erdos414.h (n : ℕ) : ℕ

Equations

• Erdos414.h n = n + n.divisors.card

theorem Erdos414.erdos_414 : sorry ↔ ∀ m > 0, ∀ n > 0, ∃ (i : ℕ) (j : ℕ), h^[i] m = h^[j] n

Let $h_1(n) = h(n)$ and $h_k(n) = h(h_{k-1}(n))$. Is it true, for any $m,n$, there exist $i$ and $j$ such that $h_i(m) = h_j(n)$?