-- There are infinitely many prime numbers. theorem inf_primes : ∀ n : ℕ, ∃ p : ℕ, n < p ∧ Nat.Prime p := fun n => (Nat.exists_infinite_primes (n + 1)).elim fun p hp => ⟨p, Nat.lt_of_...

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

-- Does there exist an odd perfect number? -- (A number n is perfect if it equals the sum of its proper divisors.) theorem no_odd_perfect : ∀ n : ℕ, Odd n → ¬(∑ d ∈ Nat.divisors n \ {n}, d = n) :=

-- Every positive integer eventually reaches 1 under the Collatz iteration. def collatzStep (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1 theorem collatz (n : ℕ) (hn : 0 < n) : ∃ k : ℕ, collatzStep^[k] n = 1 :=

-- 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) :=