For an irreducible polynomial $f \in \mathbb{Z}[x]$ with $f(n) \ge 1$ for sufficiently large $n$, does there exists a constant $c = c(f) > 0$ such that $\sum_{n \le x} \tau(f(n)) \approx c \cdot x \log x$?

1True ↔2  ∀ (f : Polynomial ℤ),3    f.natDegree ≠ 0 →4      Irreducible f →5        (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) →6          ∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)