-- There are infinitely many primes p such that p + 2 is also prime. theorem twin_prime_conjecture : ∀ N : ℕ, ∃ p : ℕ, N < p ∧ Nat.Prime p ∧ Nat.Prime (p + 2) :=