Dickson's conjecture

References:

• Wikipedia
• Arxiv

theorem Dickson.dickson_conjecture (fs : Finset (Polynomial ℤ)) (hfs : ∀ f ∈ fs, f.degree = 1 ∧ BunyakovskyCondition f) (hfs' : SchinzelCondition fs) : Infinite ↑{n : ℕ | ∀ f ∈ fs, Nat.Prime (Polynomial.eval (↑n) f).natAbs}

Dickson's conjecture If a finite set of in linear integer forms $f_i(n) = a_i n+b_i$ satisfies Schinzel condition, there exist infinitely many natural numbers $m$ such that $f_i(m)$ are primes for all $i$.

Special cases

theorem Dickson.polignac_conjecture (k : ℕ) : Infinite ↑{p : ℕ | Nat.Prime p ∧ Nat.Prime (p + 2 * k)}

Polignac's conjecture For any integer $k$ there are infinitely many primes $p$ such that $p + 2k$ is prime.

theorem Dickson.infinite_safe_primes : Infinite ↑{p : ℕ | Prime p ∧ Prime (2 * p + 1)}

The infinitude of Sophie Germain primes There are infinitely many primes $p$ such that $2p + 1$ is prime.

theorem Dickson.infinite_cousin_primes : Infinite ↑{p : ℕ | Prime p ∧ Prime (p + 4)}

The infinitude of cousin primes There are infinitely many primes $p$ such that $p + 4$ is prime.

theorem Dickson.infinite_sexy_primes : Infinite ↑{p : ℕ | Prime p ∧ Prime (p + 6)}

The infinitude of sexy primes There are infinitely many primes $p$ such that $p + 6$ is prime.