Let $f\in \mathbb{Z}[x]$ be an irreducible non-constant polynomial such that $f(n)\ge 1$ for all large $n\in \mathbb{N}$. Does there exist a constant $c=c(f)>0$ such that$$\sum _{n\le X}\tau (f(n))\sim cX\log X,$$where $\tau$ is the divisor function?

AMS 11 · open (literature)

theorem erdos_975 : answer(sorry) ↔
    ∀ f : ℤ[X], f.natDegree ≠ 0 → Irreducible f → (∀ᶠ n in atTop, 1 ≤ f.eval n) →
    ∃ c > (0 : ℝ), Tendsto (fun x ↦ Erdos975Sum f x / (x * log x)) atTop (𝓝 c)