Skip to content

Erdős problem 975

Start work

For an irreducible polynomial f∈Z[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 ∑n≤xτ(f(n))≈c⋅xlog⁡x\sum_{n \le x} \tau(f(n)) \approx c \cdot x \log x?

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

975.lean

Retained formal statement4 of 6

More concrete example for f(n)=n2+1f(n) = n^2 + 1, where the asymptote is ∑n≤xτ(n2+1)∼3πxlog⁡x+O(x)\sum_{n \le x} \tau(n^2 + 1) \sim \frac{3}{\pi} x \log x + O(x). See Tao's blog [T].

FormalConjectures/ErdosProblems/975.leanErdos975.erdos_975.variants.n2_plus_1_strong1 lineExact file
(fun x => Erdos975.Erdos975Sum (Polynomial.X ^ 2 + 1) x - 3 / Real.pi * x * Real.log x) =O[Filter.atTop] id
SolvedStatement only, no proof