All open problems
Source labels openChecked July 26, 2026

WikipediaNumber theory

Bateman-Horn Conjecture

The Bateman-Horn Conjecture* Given a finite collection of distinct irreducible polynomials non-constant f1,f2,,fkZ[x]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 ≤ x ...

Mathematical statement

The Bateman-Horn Conjecture* Given a finite collection of distinct irreducible polynomials non-constant f1,f2,,fkZ[x]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 ≤ x for which all polynomials fif_i are simultaneously prime is asymptotic to: C(f1,f2,,fk)x/(logx)kC(f_1, f_2, \dots, f_k) x / (log x)^k where CC is the Bateman-Horn constant given by the convergent infinite product: C=1DpP(11/p)(k)(1ωp/p)C = \frac{1}{D}\prod_{p\in\mathbb{P}} (1 - 1/p)^(-k) · (1 - \omega_p/p) Here ωp/p\omega_p/p is the number of residue classes modulo pp for which at least one polynomial vanishes.

The Schinzel condition ensures that for each prime pp, there exists some integer nn such that pp does not divide the product f(n)f2(n)f(n)f_(n) f_2(n) \dotsb f_(n), which guarantees the infinite product converges to a positive value.

Statement source: Wikipedia statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

bateman_horn_conjecture

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem bateman_horn_conjecture    (polys : Finset [X])    (h_nonempty : polys.Nonempty)    (h_irreducible :  f  polys, BunyakovskyCondition f)    (h_compat : SchinzelCondition polys) :    (fun x :  => (CountSimultaneousPrimes polys x : )) ~[atTop]    (fun x :  => BatemanHornConstant polys * x / (Real.log x) ^ polys.card) := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References