theorem
Schinzel.schinzel_conjecture
(fs : Finset (Polynomial ℤ))
(hfs : ∀ f ∈ fs, BunyakovskyCondition f)
(hfs' : SchinzelCondition fs)
:
Schinzel conjecture (H hypothesis) If a finite set of polynomials $f_i$ satisfies both Schinzel and Bunyakovsky conditions, there exist infinitely many natural numbers $n$ such that $f_i(n)$ are primes for all $i$.