bunyakovsky_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Bunyakovsky Conjecture: An irreducible polynomial $f \in \mathbb{Z}[x]$ with positive leading coefficient takes infinitely many prime values at positive integer inputs, provided there is no prime $p$ dividing all values $f(n)$ for $n \in \mathbb{Z}$.

The condition 'no fixed prime divisor' means: the GCD of all values $\{f(n) : n \in \mathbb{Z}\}$ equals 1. Proposed by Bunyakovsky (1857). Special cases include: $f(x) = x^2 + 1$ gives infinitely many primes (Landau's 4th problem, still open), $f(x) = 2x+1$ gives Sophie Germain primes. Generalized by Bateman–Horn conjecture (1962).

Source: Bunyakovsky, V. (1857). Mémoires de l'Académie impériale des sciences de St.-Pétersbourg (6), 6, 305–329.

Why this node was retired

The posted statement is

theorem bunyakovsky_conjecture (f : Polynomial ℤ)
    (hf1 : 0 < f.natDegree)
    (hf2 : 0 < f.leadingCoeff)
    (hf3 : ∀ p : ℕ, Nat.Prime p → ¬(∀ n : ℤ, (p : ℤ) ∣ f.eval n)) :
    {n : ℕ | Nat.Prime (f.eval (n : ℤ)).toNat ∧ 0 < f.eval (n : ℤ)}.Infinite := by
  sorry

Irreducibility stated in the prose is missing from the hypotheses.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Add Irreducible f, retaining positive degree, positive leading coefficient and no fixed prime divisor.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.