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 79 of them are formalized in Lean. We also have a page with the theorems from the list not yet in Lean.
1. The Irrationality of the Square Root of 2 #
Author: mathlib
2. Fundamental Theorem of Algebra #
Author: Chris Hughes
3. The Denumerability of the Rational Numbers #
Author: Chris Hughes
4. Pythagorean Theorem #
Author: Joseph Myers
6. Gödel’s Incompleteness Theorem #
Author: Shogo Saito
7. Law of Quadratic Reciprocity #
Author: Chris Hughes (first) and Michael Stoll (second)
9. The Area of a Circle #
Authors: James Arthur, Benjamin Davidson, and Andrew Souther
10. Euler’s Generalization of Fermat’s Little Theorem #
Author: Chris Hughes
11. The Infinitude of Primes #
Author: Jeremy Avigad
14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #
Authors: Marc Masdeu, David Loeffler
15. Fundamental Theorem of Integral Calculus #
Author: Yury G. Kudryashov (first) and Benjamin Davidson (second)
16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #
Author: Thomas Browning
17. De Moivre’s Formula #
Author: Abhimanyu Pallavi Sudhir
18. Liouville’s Theorem and the Construction of Transcendental Numbers #
Author: Jujian Zhang
19. Four Squares Theorem #
Author: Chris Hughes
20. All Primes (1 mod 4) Equal the Sum of Two Squares #
Author: Chris Hughes
22. The Non-Denumerability of the Continuum #
Author: Floris van Doorn
23. Formula for Pythagorean Triples #
Author: Paul van Wamelen
24. The Independence of the Continuum Hypothesis #
Author: Jesse Michael Han and Floris van Doorn
see the README
file in the linked repository.
25. Schroeder-Bernstein Theorem #
Author: Mario Carneiro
26. Leibniz’s Series for Pi #
Author: Benjamin Davidson
27. Sum of the Angles of a Triangle #
Author: Joseph Myers
30. The Ballot Problem #
Authors: Bhavik Mehta, Kexing Ying
31. Ramsey’s Theorem #
Author: Bhavik Mehta
34. Divergence of the Harmonic Series #
Authors: Anatole Dedecker, Yury Kudryashov
35. Taylor’s Theorem #
Author: Moritz Doll
36. Brouwer Fixed Point Theorem #
Author: Brendan Seamas Murphy
37. The Solution of a Cubic #
Author: Jeoff Lee
38. Arithmetic Mean/Geometric Mean #
Author: Yury G. Kudryashov
39. Solutions to Pell’s Equation #
Authors: Mario Carneiro (first), Michael Stoll (second)
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
42. Sum of the Reciprocals of the Triangular Numbers #
Authors: Jalex Stark, Yury Kudryashov
44. The Binomial Theorem #
Author: Chris Hughes
45. The Partition Theorem #
Authors: Bhavik Mehta, Aaron Anderson
49. The Cayley-Hamilton Theorem #
Author: Kim Morrison
51. Wilson’s Lemma #
Author: Chris Hughes
52. The Number of Subsets of a Set #
Author: mathlib
54. Königsberg Bridges Problem #
Author: Kyle Miller
55. Product of Segments of Chords #
Author: Manuel Candales
57. Heron’s Formula #
Author: Matt Kempster
58. Formula for the Number of Combinations #
Author: mathlib
59. The Laws of Large Numbers #
Author: Sébastien Gouëzel
60. Bezout’s Theorem #
Author: mathlib
62. Fair Games Theorem #
Author: Kexing Ying
63. Cantor’s Theorem #
Author: mathlib
64. L’Hopital’s Rule #
Author: Anatole Dedecker
65. Isosceles Triangle Theorem #
Author: Joseph Myers
66. Sum of a Geometric Series #
Author: Sander R. Dahmen (finite) and Johannes Hölzl (infinite)
67. e is Transcendental #
Author: Jujian Zhang
68. Sum of an arithmetic series #
Author: Johannes Hölzl
69. Greatest Common Divisor Algorithm #
Author: mathlib
70. The Perfect Number Theorem #
Author: Aaron Anderson
71. Order of a Subgroup #
Author: mathlib
72. Sylow’s Theorem #
Author: Chris Hughes
73. Ascending or Descending Sequences (Erdős–Szekeres Theorem) #
Author: Bhavik Mehta
74. The Principle of Mathematical Induction #
Author: Leonardo de Moura
Automatically generated when defining the natural numbers
75. The Mean Value Theorem #
Author: Yury G. Kudryashov
76. Fourier Series #
Author: Heather Macbeth
77. Sum of kth powers #
Authors: mathlib (Moritz Firsching, Fabian Kruse, Ashvni Narayanan)
78. The Cauchy-Schwarz Inequality #
Author: Zhouhang Zhou
79. The Intermediate Value Theorem #
Author: mathlib (Rob Lewis and Chris Hughes)
80. The Fundamental Theorem of Arithmetic #
Author: mathlib (Chris Hughes)
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 #
Authors: Manuel Candales (archive), Michael Stoll (Mathlib)
82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #
Author: Floris van Doorn
83. The Friendship Theorem #
Authors: Aaron Anderson, Jalex Stark, Kyle Miller
85. Divisibility by 3 Rule #
Author: Kim Morrison
86. Lebesgue Measure and Integration #
Author: Johannes Hölzl
88. Derangements Formula #
Author: Henry Swanson
89. The Factor and Remainder Theorems #
Author: Chris Hughes
90. Stirling’s Formula #
Authors: mathlib (Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth)
91. The Triangle Inequality #
Author: Zhouhang Zhou
93. The Birthday Problem #
Author: Eric Rodriguez
94. The Law of Cosines #
Author: Joseph Myers
95. Ptolemy’s Theorem #
Author: Manuel Candales
96. Principle of Inclusion/Exclusion #
Author: Neil Strickland
97. Cramer’s Rule #
Author: Anne Baanen
98. Bertrand’s Postulate #
Authors: Bolton Bailey, Patrick Stevens
99. Buffon Needle Problem #
Author: Enrico Z. Borba
100. Descartes Rule of Signs #
Author: Alex Meiburg