Bateman-Horn Conjecture

The question

The Bateman-Horn Conjecture Given a finite collection of distinct irreducible polynomials non-constant $f_1,f_2,\dots ,f_k\in \mathbb{Z}[x]$ with positive leading coefficients that satisfy the Schinzel condition, the number of positive integers $n\le x$ for which all polynomials $f_i$ are simultaneously prime is asymptotic to: $$\frac{C}{D}\frac{x}{(\log x{)}^k}$$ where $D={\prod }_i\mathrm{deg}(f_i)$ and $C$ is the Bateman-Horn constant given by the convergent infinite product: $$C=\prod _{p\in \mathbb{P}}(1-1/p{)}^{-k}(1-{\omega }_p/p)$$ Here ${\omega }_p$ is the number of residue classes modulo $p$ for which at least one polynomial vanishes. The product is only conditionally convergent: it is the limit as $N\to \infty$ of the partial products over the primes $p<N$.

The Schinzel condition ensures that for each prime $p$, there exists some integer $n$ such that $p$ does not divide the product $f_1(n)f_2(n)\cdots f_k(n)$, which guarantees the infinite product converges to a positive value.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.BatemanHornConjecture.

theorem bateman_horn_conjecture
    (polys : Finset ℤ[X])
    (h_nonempty : polys.Nonempty)
    (h_irreducible : ∀ f ∈ polys, BunyakovskyCondition f)
    (h_compat : SchinzelCondition polys) :
    ∃ C : ℝ, 0 < C ∧ Tendsto (BatemanHornPartialProduct polys) atTop (𝓝 C) ∧
      (fun x : ℝ => (CountSimultaneousPrimes polys x : ℝ)) ~[atTop]
        (fun x : ℝ => C / DegreesProduct polys * x / (Real.log x) ^ polys.card)

What counts as progress

• A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

Wikipedia

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.