Documentation

FormalConjectures.Paper.PrimeTuples

Prime Tuples Conjecture #

Reference: [FLC07] Friedlander, J. B. and Luca, F. and Stoiciu, M., On the irrationality of a divisor function series. Integers (2007).

theorem PrimeTuplesConjecture.prime_tuples_conjecture {k : } (hk : 2 k) (a : Fin kℕ+) (b : Fin k) (hab : ∀ (p : ), Nat.Prime p∃ (n : ), ¬p i : Fin k, ((a i) * n + b i)) :
{n : | ∀ (i : Fin k), Nat.Prime ((a i) * n + b i)}.Infinite

For any k ≥ 2, let a₁,...,aₖ and b₁,...,bₖ be integers with aᵢ > 0. Suppose that for every prime p there exists an integer n such that p ∤ ∏ i, (aᵢ n + bᵢ). Then there exist infinitely many n such that aᵢ n + bᵢ is prime for all i.