Dickson's conjecture

The question

dickson_conjecture. Dickson's conjecture If a finite set of 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$.

generalized_twin_primes. The generalized twin-prime conjecture For any positive integer $k$ there are infinitely many primes $p$ such that $p+2k$ is prime.

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

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

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

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.Dickson (5 statements).

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

theorem generalized_twin_primes (k : ℕ) (hk : 0 < k) :
    Infinite {p : ℕ | p.Prime ∧ (p + 2 * k).Prime}

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

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

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

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia
• PrimePages glossary
• OEIS Wiki
• MathWorld
• Leonard Eugene Dickson, History of the Theory of Numbers, Vol. I: Divisibility and Primality
• Arxiv

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.