The Twin Prime conjecture

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Victor Blanchi.

Created on 2022-01-26.
Last modified on 2023-05-22.

module elementary-number-theory.twin-prime-conjecture where
open import elementary-number-theory.inequality-natural-numbers
open import elementary-number-theory.natural-numbers
open import

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.universe-levels


The twin prime conjecture asserts that there are infinitely many twin primes. We assert that there are infinitely twin primes by asserting that for every n : ℕ there is a twin prime that is larger than n.

is-twin-prime-ℕ :   UU lzero
is-twin-prime-ℕ n = (is-prime-ℕ n) × (is-prime-ℕ (succ-ℕ (succ-ℕ n)))

twin-prime-conjecture : UU lzero
twin-prime-conjecture =
  (n : )  Σ   p  (is-twin-prime-ℕ p) × (leq-ℕ n p))

Recent changes