100 theorems in Lean

6 hours ago 3

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 81 of them are formalized in Lean, and 0 additional theorem(s) have just their statement formalized in Lean. We also have a page with the theorems from the list not yet in Lean.

To make updates to this list, please make a pull request to mathlib after editing the yaml source file. This can be done entirely on GitHub, see "Editing files in another user's repository".

1. The Irrationality of the Square Root of 2 #

Author: mathlib

100 theorems in Lean

1. The Irrationality of the Square Root of 2 #

2. Fundamental Theorem of Algebra #

3. The Denumerability of the Rational Numbers #

4. Pythagorean Theorem #

6. Gödel’s Incompleteness Theorem #

7. Law of Quadratic Reciprocity #

9. The Area of a Circle #

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

11. The Infinitude of Primes #

14. Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. #

15. Fundamental Theorem of Integral Calculus #

16. Insolvability of General Higher Degree Equations (Abel-Ruffini Theorem) #

17. De Moivre’s Formula #

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

19. Four Squares Theorem #

20. All Primes (1 mod 4) Equal the Sum of Two Squares #

22. The Non-Denumerability of the Continuum #

23. Formula for Pythagorean Triples #

24. The Independence of the Continuum Hypothesis #

25. Schroeder-Bernstein Theorem #

26. Leibniz’s Series for Pi #

27. Sum of the Angles of a Triangle #

30. The Ballot Problem #

31. Ramsey’s Theorem #

34. Divergence of the Harmonic Series #

35. Taylor’s Theorem #

36. Brouwer Fixed Point Theorem #

37. The Solution of a Cubic #

38. Arithmetic Mean/Geometric Mean #

39. Solutions to Pell’s Equation #

40. Minkowski’s Fundamental Theorem #

42. Sum of the Reciprocals of the Triangular Numbers #

44. The Binomial Theorem #

45. The Partition Theorem #

46. The Solution of the General Quartic Equation #

48. Dirichlet’s Theorem #

49. The Cayley-Hamilton Theorem #

51. Wilson’s Lemma #

52. The Number of Subsets of a Set #

54. Königsberg Bridges Problem #

55. Product of Segments of Chords #

57. Heron’s Formula #

58. Formula for the Number of Combinations #

59. The Laws of Large Numbers #

60. Bezout’s Theorem #

62. Fair Games Theorem #

63. Cantor’s Theorem #

64. L’Hopital’s Rule #

65. Isosceles Triangle Theorem #

66. Sum of a Geometric Series #

67. e is Transcendental #

68. Sum of an arithmetic series #

69. Greatest Common Divisor Algorithm #

70. The Perfect Number Theorem #

71. Order of a Subgroup #

72. Sylow’s Theorem #

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

74. The Principle of Mathematical Induction #

75. The Mean Value Theorem #

76. Fourier Series #

77. Sum of kth powers #

78. The Cauchy-Schwarz Inequality #

79. The Intermediate Value Theorem #

80. The Fundamental Theorem of Arithmetic #

81. Divergence of the Prime Reciprocal Series #

82. Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) #

83. The Friendship Theorem #

85. Divisibility by 3 Rule #

86. Lebesgue Measure and Integration #

88. Derangements Formula #

89. The Factor and Remainder Theorems #

90. Stirling’s Formula #

91. The Triangle Inequality #

93. The Birthday Problem #

94. The Law of Cosines #

95. Ptolemy’s Theorem #

96. Principle of Inclusion/Exclusion #

97. Cramer’s Rule #

98. Bertrand’s Postulate #