Bateman-Horn Conjecture
The Bateman-Horn Conjecture* Given a finite collection of distinct irreducible polynomials non-constant 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 with positive leading coefficients that satisfy the Schinzel condition, the number of positive integers n ≤ x for which all polynomials are simultaneously prime is asymptotic to: where is the Bateman-Horn constant given by the convergent infinite product: Here is the number of residue classes modulo for which at least one polynomial vanishes.
The Schinzel condition ensures that for each prime , there exists some integer such that does not divide the product , 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
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