-- The power set of any set has strictly greater cardinality than the set itself.
theoremcantors_theorem {α : Type*} (f : α → Set α) : ¬Function.Surjective f :=
-- The only solution to xᵃ = yᵇ + 1 with x,y,a,b > 1 is 3² = 2³ + 1.
theoremcatalan (x y a b : ℕ)
(hx : 1 < x) (hy : 1 < y) (ha : 1 < a) (hb : 1 < b)
(h : x ^ a = y ^ b + 1) :
x = 3 ∧ ...
-- No three positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for n > 2.
-- (Proved by Andrew Wiles 1995 — formalize it in Lean 4!)
theoremfermat_last (a b c n : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc ...
-- If aˣ + bʸ = cᶜ with x, y, z > 2, then a, b, c share a common prime factor.
theorembeal (a b c x y z : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(hx : 2 < x) (hy : 2 < y) (hz : 2 < z)
...
-- There is always a prime between n² and (n+1)² for every positive n.
theoremlegendre (n : ℕ) (hn : 0 < n) :
∃ p : ℕ, n^2 < p ∧ p < (n + 1)^2 ∧Nat.Prime p :=
-- Every even integer greater than 2 is the sum of two primes.
theoremgoldbach (n : ℕ) (hn : 2 < n) (heven : Even n) :
∃ p q : ℕ, Nat.Prime p ∧Nat.Prime q ∧ p + q = n :=
-- Does there exist an odd perfect number?
-- (A number n is perfect if it equals the sum of its proper divisors.)
theoremno_odd_perfect : ∀ n : ℕ, Odd n →¬(∑ d ∈ Nat.divisors n {n}, d = n) :=
-- Every positive integer eventually reaches 1 under the Collatz iteration.
defcollatzStep (n : ℕ) : ℕ := if n % 2 = 0 then n / 2 else 3 * n + 1
theoremcollatz (n : ℕ) (hn : 0 < n) :
∃ k : ℕ,...
-- There are infinitely many primes p such that p + 2 is also prime.
theoremtwin_prime_conjecture :
∀ N : ℕ, ∃ p : ℕ, N < p ∧Nat.Prime p ∧Nat.Prime (p + 2) :=