Bateman–Horn prime-counting conjecture in integral form

Open

FCP.BatemanHorn.integral_counting_conjecture

by elem · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theoryconjecturenumber-theory

Let $S$ be a nonempty finite set of distinct irreducible integer polynomials, each with positive leading coefficient and positive degree. Assume the Schinzel condition: no prime divides their product at every integer. Put $k=|S|$ and $D=\prod_{f\in S}\deg f$ . Suppose the increasing-prime Euler products converge to a positive number $C$ . The integral form of the Bateman–Horn conjecture asserts

\pi_S(x)\sim\frac{C}{D}\int_2^x\frac{dt}{(\log t)^k}\qquad(x\to\infty).

Here $\pi_S(x)$ counts natural numbers $n\le x$ for which all $|f(n)|$ are prime. This is a conjectural assertion, not a known theorem: it retains the unresolved prime-distribution content of Bateman–Horn. Existence and positivity of $C$ are hypotheses of this node and can be proved independently.

Formalization Note. The source counts positive inputs with positive prime values. Positive leading coefficients make all values positive for sufficiently large inputs, so the existing platform convention changes only finitely many counted inputs. The integral main term diverges, hence this finite change does not affect the asserted equivalence.

Preamble

import Definitions.Def_FCP_BatemanHorn

open Polynomial Filter Topology Asymptotics FCP.BatemanHorn

Formal statement

theorem FCP.BatemanHorn.integral_counting_conjecture
    (polys : Finset ℤ[X]) (h_nonempty : polys.Nonempty)
    (h_bunyakovsky : ∀ f ∈ polys, BunyakovskyCondition f)
    (h_schinzel : SchinzelCondition polys)
    (C : ℝ) (hC : 0 < C)
    (h_limit : Tendsto (partialProduct polys) atTop (𝓝 C)) :
    (fun x : ℝ => (countSimultaneousPrimes polys x : ℝ)) ~[atTop]
      (fun x : ℝ => C / degreesProduct polys *
        ∫ t in (2 : ℝ)..x, (1 : ℝ) / (Real.log t) ^ polys.card) := by sorry

Source

S. L. Aletheia-Zomlefer, L. Fukshansky and S. R. Garcia, The Bateman-Horn conjecture: Heuristics, History, and Applications, https://www1.cmc.edu/pages/faculty/lenny/papers/bateman-horn.pdf; Section 3.6, equations (3.6.1)–(3.6.3), p. 10; the natural-input/absolute-value counting convention is inherited from Definitions.Def_FCP_BatemanHorn.

View graph