This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.

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

Author: mathlib

##### 2. Fundamental Theorem of Algebra #

Author: Chris Hughes

theorem complex.exists_root {f : polynomial } (hf : 0 < f.degree) :
(z : ), f.is_root z
##### 3. The Denumerability of the Rational Numbers #

Author: Chris Hughes

##### 4. Pythagorean Theorem #

Author: Joseph Myers

theorem euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 p3 : P) :
p3 * p3 = p2 * p2 + p2 * p2 p3 =
##### 7. Law of Quadratic Reciprocity #

Author: Chris Hughes (first) and Michael Stoll (second)

theorem legendre_sym.quadratic_reciprocity {p q : } [fact (nat.prime p)] [fact (nat.prime q)] (hp : p 2) (hq : q 2) (hpq : p q) :
* = (-1) ^ (p / 2 * (q / 2))
theorem jacobi_sym.quadratic_reciprocity {a b : } (ha : odd a) (hb : odd b) :
b = (-1) ^ (a / 2 * (b / 2)) * a
##### 9. The Area of a Circle #

Authors: James Arthur, Benjamin Davidson, and Andrew Souther

mathlib archive

##### 10. Euler’s Generalization of Fermat’s Little Theorem #

Author: Chris Hughes

theorem nat.modeq.pow_totient {x n : } (h : x.coprime n) :
x ^ n.totient 1 [MOD n]
##### 11. The Infinitude of Primes #

theorem nat.exists_infinite_primes (n : ) :
(p : ), n p
##### 14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #

Authors: Marc Masdeu, David Loeffler

theorem has_sum_zeta_two  :
has_sum (λ (n : ), 1 / n ^ 2) (real.pi ^ 2 / 6)
##### 15. Fundamental Theorem of Integral Calculus #

Author: Yury G. Kudryashov (first) and Benjamin Davidson (second)

theorem interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right {E : Type u_3} [ E] {f : E} {c : E} {a b : } (hb : (nhds c)) :
has_strict_deriv_at (λ (u : ), (x : ) in a..u, f x) c b
theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le {E : Type u_3} [ E] {f : E} {a b : } {f' : E} (hab : a b) (hcont : (set.Icc a b)) (hderiv : (x : ), x b (f' x) (set.Ioi x) x) (f'int : b) :
(y : ) in a..b, f' y = f b - f a
##### 16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #

Author: Thomas Browning

mathlib archive

##### 17. De Moivre’s Formula #

Author: Abhimanyu Pallavi Sudhir

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

Author: Jujian Zhang

theorem liouville.transcendental {x : } (lx : liouville x) :
##### 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
##### 20. All Primes (1 mod 4) Equal the Sum of Two Squares #

Author: Chris Hughes

theorem nat.prime.sq_add_sq {p : } [fact (nat.prime p)] (hp : p % 4 3) :
(a b : ), a ^ 2 + b ^ 2 = p
##### 22. The Non-Denumerability of the Continuum #

Author: Floris van Doorn

##### 23. Formula for Pythagorean Triples #

Author: Paul van Wamelen

theorem pythagorean_triple.classification {x y z : } :
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))
##### 24. The Independence 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 : β α} (hf : function.injective f) (hg : function.injective g) :
(h : α β),
##### 26. Leibniz’s Series for Pi #

Author: Benjamin Davidson

theorem real.tendsto_sum_pi_div_four  :
filter.tendsto (λ (k : ), (finset.range k).sum (λ (i : ), (-1) ^ i / (2 * i + 1))) filter.at_top (nhds (real.pi / 4))
##### 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} [metric_space P] [ P] {p1 p2 p3 : P} (h2 : p2 p1) (h3 : p3 p1) :
p3 + p1 + p2 = real.pi
##### 30. The Ballot Problem #

Authors: Bhavik Mehta, Kexing Ying

mathlib archive

##### 31. Ramsey’s Theorem #

Author: Bhavik Mehta

result

##### 34. Divergence of the Harmonic Series #

Authors: Anatole Dedecker, Yury Kudryashov

##### 35. Taylor’s Theorem #

Author: Moritz Doll

theorem taylor_mean_remainder_lagrange {f : } {x x₀ : } {n : } (hx : x₀ < x) (hf : f (set.Icc x₀ x)) (hf' : (set.Icc x₀ x)) (set.Ioo x₀ x)) :
(x' : ) (hx' : x' set.Ioo x₀ x), f x - (set.Icc x₀ x) x₀ x = iterated_deriv_within (n + 1) f (set.Icc x₀ x) x' * (x - x₀) ^ (n + 1) / ((n + 1).factorial)
theorem taylor_mean_remainder_cauchy {f : } {x x₀ : } {n : } (hx : x₀ < x) (hf : f (set.Icc x₀ x)) (hf' : (set.Icc x₀ x)) (set.Ioo x₀ x)) :
(x' : ) (hx' : x' set.Ioo x₀ x), f x - (set.Icc x₀ x) x₀ x = iterated_deriv_within (n + 1) f (set.Icc x₀ x) x' * (x - x') ^ n / (n.factorial) * (x - x₀)
##### 36. Brouwer Fixed Point Theorem #

Author: Brendan Seamas Murphy

result

##### 37. The Solution of a Cubic #

Author: Jeoff Lee

mathlib archive

##### 38. Arithmetic Mean/Geometric Mean #

Author: Yury G. Kudryashov

theorem real.geom_mean_le_arith_mean_weighted {ι : Type u} (s : finset ι) (w z : ι ) (hw : (i : ι), i s 0 w i) (hw' : s.sum (λ (i : ι), w i) = 1) (hz : (i : ι), i s 0 z i) :
s.prod (λ (i : ι), z i ^ w i) s.sum (λ (i : ι), w i * z i)
##### 39. Solutions to Pell’s Equation #

Authors: Mario Carneiro (first), Michael Stoll (second)

theorem pell.eq_pell {a : } (a1 : 1 < a) {x y : } (hp : x * x - d a1 * y * y = 1) :
(n : ), x = pell.xn a1 n y = pell.yn a1 n
theorem pell.exists_of_not_is_square {d : } (h₀ : 0 < d) (hd : ¬) :
(x y : ), x ^ 2 - d * y ^ 2 = 1 y 0

In pell.eq_pell, d is defined to be a*a - 1 for an arbitrary a > 1.

##### 40. Minkowski’s Fundamental Theorem #

Authors: Alex J. Best, Yaël Dillies

theorem measure_theory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure {E : Type u_1} {μ : measure_theory.measure E} {F s : set E} [ E] [borel_space E] {L : add_subgroup E} [countable L] (fund : μ) (h : μ F * 2 ^ fdim E < μ s) (h_symm : (x : E), x s -x s) (h_conv : s) :
(x : L) (H : x 0), x s
##### 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 {R : Type u_1} (x y : R) (n : ) :
(x + y) ^ n = (finset.range (n + 1)).sum (λ (m : ), x ^ m * y ^ (n - m) * (n.choose m))
##### 45. The Partition Theorem #

Authors: Bhavik Mehta, Aaron Anderson

mathlib archive

##### 49. The Cayley-Hamilton Theorem #

Author: Scott Morrison

theorem matrix.aeval_self_charpoly {R : Type u} [comm_ring R] {n : Type w} [decidable_eq n] [fintype n] (M : n R) :
= 0
##### 51. Wilson’s Lemma #

Author: Chris Hughes

theorem zmod.wilsons_lemma (p : ) [fact (nat.prime p)] :
((p - 1).factorial) = -1
##### 52. The Number of Subsets of a Set #

Author: mathlib

theorem finset.card_powerset {α : Type u_1} (s : finset α) :
##### 54. Königsberg Bridges Problem #

Author: Kyle Miller

mathlib archive

##### 55. Product of Segments of Chords #

Author: Manuel Candales

theorem euclidean_geometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapb : = real.pi) (hcpd : = real.pi) :
* = *
##### 57. Heron’s Formula #

Author: Matt Kempster

mathlib archive

##### 58. Formula for the Number of Combinations #

Author: mathlib

theorem finset.card_powerset_len {α : Type u_1} (n : ) (s : finset α) :
s).card = s.card.choose n
theorem finset.mem_powerset_len {α : Type u_1} {n : } {s t : finset α} :
s s t s.card = n
##### 59. The Laws of Large Numbers #

Author: Sébastien Gouëzel

theorem probability_theory.strong_law_ae {Ω : Type u_1} (X : Ω ) (hindep : pairwise (λ (i j : ), ) (hident : (i : ), ) :
∀ᵐ (ω : Ω), filter.tendsto (λ (n : ), (finset.range n).sum (λ (i : ), X i ω) / n) filter.at_top (nhds ( (a : Ω), X 0 a))
##### 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
##### 62. Fair Games Theorem #

Author: Kexing Ying

theorem measure_theory.submartingale_iff_expected_stopped_value_mono {Ω : Type u_1} {m0 : measurable_space Ω} {μ : measure_theory.measure Ω} {𝒢 : m0} {f : Ω } (hadp : f) (hint : (i : ), μ) :
(τ π : Ω ), τ π ( (N : ), (x : Ω), π x N) (x : Ω), μ (x : Ω), μ
##### 63. Cantor’s Theorem #

Author: mathlib

theorem cardinal.cantor (a : cardinal) :
a < 2 ^ a
##### 64. L’Hopital’s Rule #

Author: Anatole Dedecker

theorem deriv.lhopital_zero_nhds {a : } {l : filter } {f g : } (hdf : ∀ᶠ (x : ) in nhds a, ) (hg' : ∀ᶠ (x : ) in nhds a, x 0) (hfa : (nhds a) (nhds 0)) (hga : (nhds a) (nhds 0)) (hdiv : filter.tendsto (λ (x : ), x / x) (nhds a) l) :
filter.tendsto (λ (x : ), f x / g x) {a}) l
##### 65. Isosceles Triangle Theorem #

Author: Joseph Myers

theorem euclidean_geometry.angle_eq_angle_of_dist_eq {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {p1 p2 p3 : P} (h : p2 = p3) :
p3 = p2
##### 66. Sum of a Geometric Series #

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

theorem geom_sum_Ico {α : Type u} {x : α} (hx : x 1) {m n : } (hmn : m n) :
n).sum (λ (i : ), x ^ i) = (x ^ n - x ^ m) / (x - 1)
theorem nnreal.has_sum_geometric {r : nnreal} (hr : r < 1) :
has_sum (λ (n : ), r ^ n) (1 - r)⁻¹
##### 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 : ) :
(finset.range n).sum (λ (i : ), i) = n * (n - 1) / 2
##### 69. Greatest Common Divisor Algorithm #

Author: mathlib

def euclidean_domain.gcd {R : Type u} [decidable_eq R] :
R R R
theorem euclidean_domain.gcd_dvd {R : Type u} [decidable_eq R] (a b : R) :
theorem euclidean_domain.dvd_gcd {R : Type u} [decidable_eq R] {a b c : R} :
c a c b
##### 70. The Perfect Number Theorem #

Author: Aaron Anderson

mathlib archive

##### 71. Order of a Subgroup #

Author: mathlib

theorem subgroup.card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] :
##### 72. Sylow’s Theorem #

Author: Chris Hughes

theorem sylow.exists_subgroup_card_pow_prime {G : Type u} [group G] [fintype G] (p : ) {n : } [fact (nat.prime p)] (hdvd : p ^ n ) :
(K : subgroup G), = p ^ n

sylow_conjugate

card_sylow_dvd

card_sylow_modeq_one

##### 73. Ascending or Descending Sequences (Erdős–Szekeres Theorem) #

Author: Bhavik Mehta

mathlib archive

##### 74. The Principle of Mathematical Induction #

Author: Leonardo de Moura

inductive nat  :

Automatically generated when defining the natural numbers

##### 75. The Mean Value Theorem #

Author: Yury G. Kudryashov

theorem exists_deriv_eq_slope (f : ) {a b : } (hab : a < b) (hfc : (set.Icc a b)) (hfd : (set.Ioo a b)) :
(c : ) (H : c b), c = (f b - f a) / (b - a)
##### 76. Fourier Series #

Author: Heather Macbeth

noncomputable def fourier_coeff {T : } [hT : fact (0 < T)] {E : Type} [ E] (f : E) (n : ) :
E
theorem has_sum_fourier_series_L2 {T : } [hT : fact (0 < T)]  :
has_sum (λ (i : ), i) f
##### 77. Sum of kth powers #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)

theorem sum_range_pow (n p : ) :
(finset.range n).sum (λ (k : ), k ^ p) = (finset.range (p + 1)).sum (λ (i : ), * ((p + 1).choose i) * n ^ (p + 1 - i) / (p + 1))
theorem sum_Ico_pow (n p : ) :
(n + 1)).sum (λ (k : ), k ^ p) = (finset.range (p + 1)).sum (λ (i : ), * ((p + 1).choose i) * n ^ (p + 1 - i) / (p + 1))
##### 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 𝕜] [ E] (x y : E) :
theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [ E] (x y : E) :
##### 79. The Intermediate Value Theorem #

Author: mathlib (Rob Lewis and Chris Hughes)

theorem intermediate_value_Icc {α : Type u} {δ : Type u_1} [linear_order δ] {a b : α} (hab : a b) {f : α δ} (hf : (set.Icc a b)) :
set.Icc (f a) (f b) f '' b
##### 80. The Fundamental Theorem of Arithmetic #

Author: mathlib (Chris Hughes)

theorem nat.factors_unique {n : } {l : list } (h₁ : l.prod = n) (h₂ : (p : ), p l ) :
structure unique_factorization_monoid (α : Type u_2)  :
Prop
theorem unique_factorization_monoid.factors_unique {α : Type u_1} {f g : multiset α} (hf : (x : α), x f ) (hg : (x : α), x g ) (h : g.prod) :

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.

##### 81. Divergence of the Prime Reciprocal Series #

Author: Manuel Candales

mathlib archive

##### 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
##### 86. Lebesgue Measure and Integration #

Author: Johannes Hölzl

noncomputable def measure_theory.lintegral {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (f : α ennreal) :
##### 88. Derangements Formula #

Author: Henry Swanson

theorem num_derangements_sum (n : ) :
= (finset.range (n + 1)).sum (λ (k : ), (-1) ^ k * (k.asc_factorial (n - k)))
##### 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} :
theorem polynomial.mod_X_sub_C_eq_C_eval {R : Type u} [field R] (p : polynomial R) (a : R) :
p % =
##### 90. Stirling’s Formula #

Authors: mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)

##### 91. The Triangle Inequality #

Author: Zhouhang Zhou

theorem norm_add_le {E : Type u_6} (a b : E) :
##### 93. The Birthday Problem #

Author: Eric Rodriguez

mathlib archive

##### 94. The Law of Cosines #

Author: Joseph Myers

theorem euclidean_geometry.dist_sq_eq_dist_sq_add_dist_sq_sub_two_mul_dist_mul_dist_mul_cos_angle {V : Type u_1} {P : Type u_2} [metric_space P] [ P] (p1 p2 p3 : P) :
p3 * p3 = p2 * p2 + p2 * p2 - 2 * p2 * p2 * real.cos p2 p3)
##### 95. Ptolemy’s Theorem #

Author: Manuel Candales

theorem euclidean_geometry.mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {V : Type u_1} {P : Type u_2} [metric_space P] [ P] {a b c d p : P} (h : euclidean_geometry.cospherical {a, b, c, d}) (hapc : = real.pi) (hbpd : = real.pi) :
* + * = *
##### 96. Principle of Inclusion/Exclusion #

Author: Neil Strickland

github

##### 97. Cramer’s Rule #

Author: Anne Baanen

theorem matrix.mul_vec_cramer {n : Type v} {α : Type w} [decidable_eq n] [fintype n] [comm_ring α] (A : n α) (b : n α) :
A.mul_vec ((A.cramer) b) = A.det b
##### 98. Bertrand’s Postulate #

Authors: Bolton Bailey, Patrick Stevens

theorem nat.bertrand (n : ) (hn0 : n 0) :
(p : ), n < p p 2 * n