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 52 of them are formalized in Lean. We also have a page with the theorems from the list not yet in mathlib.

1. The Irrationality of the Square Root of 2 #

Author: mathlib

docs, source

2. Fundamental Theorem of Algebra #

Author: Chris Hughes

theorem 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

docs, source

4. Pythagorean Theorem #

Author: Joseph Myers

theorem 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] [normed_add_torsor V P] (p1 p2 p3 : P) :
(dist p1 p3) * dist p1 p3 = (dist p1 p2) * dist p1 p2 + (dist p3 p2) * dist p3 p2 p1 p2 p3 = π / 2

docs, source

7. Law of Quadratic Reciprocity #

Author: Chris Hughes

theorem zmod.quadratic_reciprocity (p q : ) [fact (nat.prime p)] [fact (nat.prime q)] [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

theorem nat.modeq.pow_totient {x n : } :
x.coprime nx ^ n.totient 1 [MOD n]

docs, source

11. The Infinitude of Primes #

Author: Jeremy Avigad

theorem nat.exists_infinite_primes (n : ) :
∃ (p : ), n p nat.prime p

docs, source

17. De Moivre’s Theorem #

Author: Abhimanyu Pallavi Sudhir

docs, source

18. Liouville’s Theorem and the Construction of Transcendental Numbers #

Author: Jujian Zhang

result

website

19. Four Squares Theorem #

Author: Chris Hughes

theorem 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

theorem nat.prime.sum_two_squares (p : ) [hp : fact (nat.prime p)] :
p % 4 = 1(∃ (a b : ), a ^ 2 + b ^ 2 = p)

docs, source

22. The Non-Denumerability of the Continuum #

Author: Floris van Doorn

docs, source

23. Formula for Pythagorean Triples #

Author: Paul van Wamelen

theorem pythagorean_triple.classification {x y z : } :
pythagorean_triple x y z ∃ (k m n : ), (x = k * (m ^ 2 - n ^ 2) y = k * (2 * m) * n x = k * (2 * m) * n y = k * (m ^ 2 - n ^ 2)) (z = k * (m ^ 2 + n ^ 2) z = (-k) * (m ^ 2 + n ^ 2))

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

theorem function.embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} :
function.injective ffunction.injective g(∃ (h : α → β), function.bijective h)

docs, source

26. Leibniz’s Series for Pi #

Author: Benjamin Davidson

theorem real.tendsto_sum_pi_div_four  :
filter.tendsto (λ (k : ), ∑ (i : ) in finset.range k, (-1) ^ i / (2 * i + 1)) filter.at_top (𝓝 (π / 4))

docs, source

27. Sum of the Angles of a Triangle #

Author: Joseph Myers

theorem euclidean_geometry.angle_add_angle_add_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} :
p2 p1p3 p1 p1 p2 p3 + p2 p3 p1 + p3 p1 p2 = π

docs, source

31. Ramsey’s Theorem #

Author: Bhavik Mehta

result

34. Divergence of the Harmonic Series #

Author: Anatole Dedecker

docs, source

38. Arithmetic Mean/Geometric Mean #

Author: Yury G. Kudryashov

theorem real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : finset ι) (w z : ι → ) :
(∀ (i : ι), i s0 w i)∑ (i : ι) in s, w i = 1(∀ (i : ι), i s0 z i)∏ (i : ι) in s, z i ^ w i ∑ (i : ι) in s, (w i) * z i

docs, source

39. Solutions to Pell’s Equation #

Author: Mario Carneiro

theorem 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 #

Authors: Jalex Stark, Yury Kudryashov

mathlib archive

44. The Binomial Theorem #

Author: Chris Hughes

theorem add_pow {α : Type u_1} [comm_semiring α] (x y : α) (n : ) :
(x + y) ^ n = ∑ (m : ) in finset.range (n + 1), ((x ^ m) * y ^ (n - m)) * (n.choose m)

docs, source

49. The Cayley-Hamilton Theorem #

Author: Scott Morrison

theorem aeval_self_char_poly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : matrix n n R) :

docs, source

51. Wilson’s Theorem #

Author: Chris Hughes

theorem zmod.wilsons_lemma (p : ) [fact (nat.prime p)] :
(p - 1)! = -1

docs, source

52. The Number of Subsets of a Set #

Author: mathlib

theorem finset.card_powerset {α : Type u_1} (s : finset α) :

docs, source

58. Formula for the Number of Combinations #

Author: mathlib

theorem finset.card_powerset_len {α : Type u_1} (n : ) (s : finset α) :

docs, source

theorem finset.mem_powerset_len {α : Type u_1} {n : } {s t : finset α} :

docs, source

60. Bezout’s Theorem #

Author: mathlib

theorem 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

theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a

docs, source

64. L’Hopital’s Rule #

Author: Anatole Dedecker

theorem deriv.lhopital_zero_nhds {a : } {l : filter } {f g : } :
(∀ᶠ (x : ) in 𝓝 a, differentiable_at f x)(∀ᶠ (x : ) in 𝓝 a, deriv g x 0)filter.tendsto f (𝓝 a) (𝓝 0)filter.tendsto g (𝓝 a) (𝓝 0)filter.tendsto (λ (x : ), deriv f x / deriv g x) (𝓝 a) lfilter.tendsto (λ (x : ), f x / g x) (𝓝[set.univ \ {a}] a) l

docs, source

65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem euclidean_geometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} :
dist p1 p2 = dist p1 p3 p1 p2 p3 = p1 p3 p2

docs, source

66. Sum of a Geometric Series #

Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)

theorem geom_sum {α : Type u} [division_ring α] {x : α} (h : x 1) (n : ) :
geom_series x n = (x ^ n - 1) / (x - 1)

docs, source

theorem nnreal.has_sum_geometric {r : ℝ≥0} :
r < 1has_sum (λ (n : ), r ^ n) (1 - r)⁻¹

docs, source

67. e is Transcendental #

Author: Jujian Zhang

result

website

68. Sum of an arithmetic series #

Author: Johannes Hölzl

theorem finset.sum_range_id (n : ) :
∑ (i : ) in finset.range n, i = n * (n - 1) / 2

docs, source

69. Greatest Common Divisor Algorithm #

Author: mathlib

def euclidean_domain.gcd {R : Type u} [euclidean_domain R] [decidable_eq R] :
R → R → R

docs, source

docs, source

theorem euclidean_domain.dvd_gcd {R : Type u} [euclidean_domain R] [decidable_eq R] {a b c : R} :
c ac bc euclidean_domain.gcd a b

docs, source

70. The Perfect Number Theorem #

Author: Aaron Anderson

mathlib archive

71. Order of a Subgroup #

Author: mathlib

theorem card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] :

docs, source

72. Sylow’s Theorem #

Author: Chris Hughes

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ) {n : } [hp : fact (nat.prime p)] :
p ^ n fintype.card G(∃ (H : subgroup G), 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

inductive nat  :
Type

docs, source

Automatically generated when defining the natural numbers

75. The Mean Value Theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_slope (f : ) {a b : } :
a < bcontinuous_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

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :

docs, source

theorem abs_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :

docs, source

79. The Intermediate Value Theorem #

Author: mathlib (Rob Lewis and Chris Hughes)

theorem 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)

theorem nat.factors_unique {n : } {l : list } :
l.prod = n(∀ (p : ), p lnat.prime p)l ~ n.factors

docs, source

docs, source

docs, source

structure unique_factorization_monoid (α : Type u_2) [comm_cancel_monoid_with_zero α] :
Prop

docs, source

theorem unique_factorization_monoid.factors_unique {α : Type u_1} [comm_cancel_monoid_with_zero α] [unique_factorization_monoid α] {f g : multiset α} :
(∀ (x : α), x firreducible x)(∀ (x : α), x girreducible x)associated f.prod g.prodmultiset.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

83. The Friendship Theorem #

Authors: Aaron Anderson, Jalex Stark, Kyle Miller

mathlib archive

85. Divisibility by 3 Rule #

Author: Scott Morrison

theorem nat.three_dvd_iff (n : ) :
3 n 3 (10.digits n).sum

docs, source

86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

def measure_theory.lintegral {α : Type u_1} [measurable_space α] :

docs, source

89. The Factor and Remainder Theorems #

Author: Chris Hughes

theorem polynomial.dvd_iff_is_root {R : Type u} {a : R} [comm_ring R] {p : polynomial R} :

docs, source

docs, source

91. The Triangle Inequality #

Author: Zhouhang Zhou

theorem norm_add_le {α : Type u_1} [normed_group α] (g h : α) :

docs, source

94. The Law of Cosines #

Author: Joseph Myers

theorem 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] [normed_add_torsor V P] (p1 p2 p3 : P) :
(dist p1 p3) * dist p1 p3 = (dist p1 p2) * dist p1 p2 + (dist p3 p2) * dist p3 p2 - ((2 * dist p1 p2) * dist p3 p2) * real.cos ( p1 p2 p3)

docs, source

96. Principle of Inclusion/Exclusion #

Author: Neil Strickland

github