Skip to content

Erdős problem 975

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 statement5 of 6

When ff is an irreducible quadratic polynomial, the question is answered first by Hooley [Ho63]. More compact expression of the constant in terms of Hurwitz class numbers (when a=1a = 1) is given by McKey in [Mc95], [Mc97], [Mc99].

TODO: formalize Hurwitz class numbers and the expression of the constant in terms of them.

FormalConjectures/ErdosProblems/975.leanErdos975.erdos_975.variants.quadratic7 linesExact file
∀ (f : Polynomial ℤ),  Irreducible f →    (∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ Polynomial.eval (↑n) f) →      f.degree = 2 →        ∀ (c : ℝ),          c = sorry →            0 < c ∧ Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)
SolvedStatement only, no proof