-- There are infinitely many primes of the form 2ⁿ - 1. theorem inf_mersenne_primes : ∀ N : ℕ, ∃ n : ℕ, N < n ∧ Nat.Prime (2^n - 1) :=