Skip to content

Erdős problem 975

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

6 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

975.lean

Retained formal statement1 of 6

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

Note that it is unclear whether the polynomial should have integer coefficients or merely be integer-valued. We assume the former.

FormalConjectures/ErdosProblems/975.leanErdos975.erdos_9756 linesExact file
True  ∀ (f : Polynomial ℤ),    f.natDegree ≠ 0 →      Irreducible f        (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) →c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page