theorem
Bunyakovsky.bunyakovsky_conjecture
(f : Polynomial ℤ)
:
BunyakovskyCondition f ∧ SchinzelCondition {f} → Infinite ↑{n : ℕ | Nat.Prime (Polynomial.eval (↑n) f).natAbs}
Bunyakovsky conjecture If a polynomial $f$ over integers satisfies both Schinzel and Bunyakovsky conditions, there exist infinitely many natural numbers $m$ such that $f(m)$ is prime.