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