100 theorems

Freek Wiedijk maintains a list tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers. Currently 43 of them are formalized in Lean:

1: The Irrationality of the Square Root of 2 #
Author: mathlib
irrational_sqrt_two :
irrational 2.sqrt

docs, source

2: Fundamental Theorem of Algebra #
Author: Chris Hughes
complex.exists_root {f : polynomial ℂ} :
0 < f.degree → (∃ (z : ℂ), f.is_root z)

docs, source

3: The Denumerability of the Rational Numbers #
Author: Chris Hughes
rat.denumerable :
denumerable ℚ

docs, source

4: Pythagorean Theorem #
Author: Joseph Myers
euclidean_geometry.dist_square_eq_dist_square_add_dist_square_iff_angle_eq_pi_div_two (V : Type u_1) {P : Type u_2} [inner_product_space V] [metric_space P] [euclidean_affine_space V P] (p1 p2 p3 : P) :
has_dist.dist p1 p3 * has_dist.dist p1 p3 = has_dist.dist p1 p2 * has_dist.dist p1 p2 + has_dist.dist p3 p2 * has_dist.dist p3 p2 ↔ euclidean_geometry.angle V p1 p2 p3 = real.pi / 2

docs, source

7: Law of Quadratic Reciprocity #
Author: Chris Hughes
zmod.quadratic_reciprocity (p q : ℕ) [fact p.prime] [fact q.prime] [hp1 : fact (p % 2 = 1)] [hq1 : fact (q % 2 = 1)] :
p ≠ q → zmod.legendre_sym p q * zmod.legendre_sym q p = (-1) ^ (p / 2 * (q / 2))

docs, source

10: Euler’s Generalization of Fermat’s Little Theorem #
Author: Chris Hughes
nat.modeq.pow_totient {x n : ℕ} :
x.coprime n → x ^ n.totient ≡ 1 [MOD n]

docs, source

11: The Infinitude of Primes #
Author: Jeremy Avigad
nat.exists_infinite_primes (n : ℕ) :
∃ (p : ℕ), n ≤ p ∧ p.prime

docs, source

17: De Moivre’s Theorem #
Author: Abhimanyu Pallavi Sudhir
complex.cos_add_sin_mul_I_pow (n : ℕ) (z : ℂ) :
(complex.cos z + complex.sin z * complex.I) ^ n = complex.cos (↑n * z) + complex.sin (↑n * z) * complex.I

docs, source

19: Four Squares Theorem #
Author: Chris Hughes
nat.sum_four_squares (n : ℕ) :
∃ (a b c d : ℕ), a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

docs, source

20: All Primes (1 mod 4) Equal the Sum of Two Squares #
Author: Chris Hughes
nat.prime.sum_two_squares (p : ℕ) [hp : fact p.prime] :
p % 4 = 1 → (∃ (a b : ℕ), a ^ 2 + b ^ 2 = p)

docs, source

22: The Non-Denumerability of the Continuum #
Author: Floris van Doorn
cardinal.not_countable_real :
¬set.univ.countable

docs, source

24: The Undecidability of the Continuum Hypothesis #
Author: Jesse Michael Han and Floris van Doorn

result

website

see the README file in the linked repository.

25: Schroeder-Bernstein Theorem #
Author: Mario Carneiro
function.embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} :
function.injective f → function.injective g → (∃ (h : α → β), function.bijective h)

docs, source

27: Sum of the Angles of a Triangle #
Author: Joseph Myers
euclidean_geometry.angle_add_angle_add_angle_eq_pi (V : Type u_1) {P : Type u_2} [inner_product_space V] [metric_space P] [euclidean_affine_space V P] {p1 p2 p3 : P} :
p2 ≠ p1 → p3 ≠ p1 → euclidean_geometry.angle V p1 p2 p3 + euclidean_geometry.angle V p2 p3 p1 + euclidean_geometry.angle V p3 p1 p2 = real.pi

docs, source

31: Ramsey’s Theorem #
Author: Bhavik Mehta

result

38: Arithmetic Mean/Geometric Mean #
Author: Yury G. Kudryashov
real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : finset ι) (w z : ι → ℝ) :
(∀ (i : ι), i ∈ s → 0 ≤ w i) → s.sum (λ (i : ι), w i) = 1 → (∀ (i : ι), i ∈ s → 0 ≤ z i) → s.prod (λ (i : ι), z i ^ w i) ≤ s.sum (λ (i : ι), w i * z i)

docs, source

39: Solutions to Pell’s Equation #
Author: Mario Carneiro
pell.eq_pell {a : ℕ} (a1 : 1 < a) {x y : ℕ} :
x * x - d a1 * y * y = 1 → (∃ (n : ℕ), x = pell.xn a1 n ∧ y = pell.yn a1 n)

docs, source

d is defined to be a*a - 1 for an arbitrary a > 1.

42: Sum of the Reciprocals of the Triangular Numbers #
Author: Jalex Stark, Yury Kudryashov

mathlib archive

44: The Binomial Theorem #
Author: Chris Hughes
add_pow {α : Type u_1} [comm_semiring α] (x y : α) (n : ℕ) :
(x + y) ^ n = (finset.range (n + 1)).sum (λ (m : ℕ), x ^ m * y ^ (n - m) * ↑(n.choose m))

docs, source

51: Wilson’s Theorem #
Author: Chris Hughes
zmod.wilsons_lemma (p : ℕ) [fact p.prime] :
↑((p - 1).fact) = -1

docs, source

52: The Number of Subsets of a Set #
Author: mathlib
finset.card_powerset {α : Type u_1} (s : finset α) :
s.powerset.card = 2 ^ s.card

docs, source

58: Formula for the Number of Combinations #
Author: mathlib
finset.card_powerset_len {α : Type u_1} (n : ℕ) (s : finset α) :
(finset.powerset_len n s).card = s.card.choose n

docs, source

finset.mem_powerset_len {α : Type u_1} {n : ℕ} {s t : finset α} :
s ∈ finset.powerset_len n t ↔ s ⊆ t ∧ s.card = n

docs, source

60: Bezout’s Theorem #
Author: mathlib
nat.gcd_eq_gcd_ab (x y : ℕ) :
↑(x.gcd y) = ↑x * x.gcd_a y + ↑y * x.gcd_b y

docs, source

63: Cantor’s Theorem #
Author: mathlib
cardinal.cantor (a : cardinal) :
a < 2 ^ a

docs, source

65: Isosceles Triangle Theorem #
Author: Joseph Myers
euclidean_geometry.angle_eq_angle_of_dist_eq (V : Type u_1) {P : Type u_2} [inner_product_space V] [metric_space P] [euclidean_affine_space V P] {p1 p2 p3 : P} :
has_dist.dist p1 p2 = has_dist.dist p1 p3 → euclidean_geometry.angle V p1 p2 p3 = euclidean_geometry.angle V p1 p3 p2

docs, source

66: Sum of a Geometric Series #
Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)
geom_sum {α : Type u} [division_ring α] {x : α} (h : x ≠ 1) (n : ℕ) :
geom_series x n = (x ^ n - 1) / (x - 1)

docs, source

nnreal.has_sum_geometric {r : nnreal} :
r < 1 → has_sum (λ (n : ℕ), r ^ n) (1 - r)⁻¹

docs, source

68: Sum of an arithmetic series #
Author: Johannes Hölzl
finset.sum_range_id (n : ℕ) :
(finset.range n).sum (λ (i : ℕ), i) = n * (n - 1) / 2

docs, source

69: Greatest Common Divisor Algorithm #
Author: mathlib
euclidean_domain.gcd {α : Type u} [euclidean_domain α] [decidable_eq α] :
α → α → α

docs, source

euclidean_domain.gcd_dvd {α : Type u} [euclidean_domain α] [decidable_eq α] (a b : α) :
euclidean_domain.gcd a b ∣ a ∧ euclidean_domain.gcd a b ∣ b

docs, source

euclidean_domain.dvd_gcd {α : Type u} [euclidean_domain α] [decidable_eq α] {a b c : α} :
c ∣ a → c ∣ b → c ∣ euclidean_domain.gcd a b

docs, source

71: Order of a Subgroup #
Author: mathlib
card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : set α) [is_subgroup s] [fintype ↥s] :
fintype.card ↥s ∣ fintype.card α

docs, source

72: Sylow’s Theorem #
Author: Chris Hughes
sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ℕ) {n : ℕ} [hp : fact p.prime] :
p ^ n ∣ fintype.card G → (∃ (H : set G), is_subgroup H ∧ fintype.card ↥H = p ^ n)

docs, source

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

73: Ascending or Descending Sequences #
Author: Bhavik Mehta

mathlib archive

74: The Principle of Mathematical Induction #
Author: Leonardo de Moura
nat :
Type

docs, source

Automatically generated when defining the natural numbers

75: The Mean Value Theorem #
Author: Yury G. Kudryashov
exists_deriv_eq_slope (f : ℝ → ℝ) {a b : ℝ} :
a < b → continuous_on f (set.Icc a b) → differentiable_on ℝ f (set.Ioo a b) → (∃ (c : ℝ) (H : c ∈ set.Ioo a b), deriv f c = (f b - f a) / (b - a))

docs, source

78: The Cauchy-Schwarz Inequality #
Author: Zhouhang Zhou
inner_mul_inner_self_le {α : Type u} [inner_product_space α] (x y : α) :
has_inner.inner x y * has_inner.inner x y ≤ has_inner.inner x x * has_inner.inner y y

docs, source

abs_inner_le_norm {α : Type u} [inner_product_space α] (x y : α) :
abs (has_inner.inner x y) ≤ ∥x∥ * ∥y∥

docs, source

79: The Intermediate Value Theorem #
Author: mathlib (Rob Lewis and Chris Hughes)
intermediate_value_Icc {α : Type u} {β : Type v} [conditionally_complete_linear_order α] [topological_space α] [order_topology α] [conditionally_complete_linear_order β] [topological_space β] [order_topology β] [densely_ordered α] {a b : α} (hab : a ≤ b) {f : α → β} :
continuous_on f (set.Icc a b) → set.Icc (f a) (f b) ⊆ f '' set.Icc a b

docs, source

80: The Fundamental Theorem of Arithmetic #
Author: mathlib (Chris Hughes)
nat.factors_unique {n : ℕ} {l : list ℕ} :
l.prod = n → (∀ (p : ℕ), p ∈ l → p.prime) → l ~ n.factors

docs, source

int.euclidean_domain :
euclidean_domain ℤ

docs, source

euclidean_domain.to_principal_ideal_domain {R : Type u} [euclidean_domain R] :
is_principal_ideal_ring R

docs, source

unique_factorization_domain (α : Type u_2) [integral_domain α] :
Type u_2

docs, source

unique_factorization_domain.unique {α : Type u_1} [integral_domain α] [unique_factorization_domain α] {f g : multiset α} :
(∀ (x : α), x ∈ f → irreducible x) → (∀ (x : α), x ∈ g → irreducible x) → associated f.prod g.prod → multiset.rel associated f g

docs, source

it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain.

82: Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #
Author: Floris van Doorn

mathlib archive

85: Divisibility by 3 Rule #
Author: Scott Morrison
three_dvd_iff (n : ℕ) :
3 ∣ n ↔ 3 ∣ (digits 10 n).sum

docs, source

86: Lebesgue Measure and Integration #
Author: Johannes Hölzl
measure_theory.lintegral {α : Type u_1} [measure_theory.measure_space α] :
(α → ennreal) → ennreal

docs, source

89: The Factor and Remainder Theorems #
Author: Chris Hughes
polynomial.dvd_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :
polynomial.X - ⇑polynomial.C a ∣ p ↔ p.is_root a

docs, source

polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [field R] (p : polynomial R) (a : R) :
p % (polynomial.X - ⇑polynomial.C a) = ⇑polynomial.C (polynomial.eval a p)

docs, source

91: The Triangle Inequality #
Author: Zhouhang Zhou
inner_product_space.to_normed_group :
normed_group α

docs, source

94: The Law of Cosines #
Author: Joseph Myers
euclidean_geometry.dist_square_eq_dist_square_add_dist_square_sub_two_mul_dist_mul_dist_mul_cos_angle (V : Type u_1) {P : Type u_2} [inner_product_space V] [metric_space P] [euclidean_affine_space V P] (p1 p2 p3 : P) :
has_dist.dist p1 p3 * has_dist.dist p1 p3 = has_dist.dist p1 p2 * has_dist.dist p1 p2 + has_dist.dist p3 p2 * has_dist.dist p3 p2 - 2 * has_dist.dist p1 p2 * has_dist.dist p3 p2 * real.cos (euclidean_geometry.angle V p1 p2 p3)

docs, source

96: Principle of Inclusion/Exclusion #
Author: Neil Strickland

github