Freek Wiedijk's 100 theorems

Freek Wiedijk's list of 100 famous theorems, with Mathlib's formalizations (docs/100.yaml). Mathlib does not have 21 of its 100 items; they have no article here.

Theorems 1 to 27

• 1. The Irrationality of the Square Root of 2
• 2. Fundamental Theorem of Algebra
• 3. The Denumerability of the Rational Numbers
• 4. Pythagorean 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
• 25. Schroeder-Bernstein Theorem
• 26. Leibniz’s Series for Pi
• 27. Sum of the Angles of a Triangle

Theorems 30 to 57

• 30. The Ballot Problem
• 33. Fermat’s Last Theorem
• 34. Divergence of the Harmonic Series
• 35. Taylor’s 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
• 47. The Central Limit Theorem
• 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

Theorems 58 to 78

• 58. Formula for the Number of Combinations
• 59. The Laws of Large Numbers
• 60. Bezout’s Theorem
• 61. Theorem of Ceva
• 62. Fair Games Theorem
• 63. Cantor’s Theorem
• 64. L’Hopital’s Rule
• 65. Isosceles Triangle Theorem
• 66. Sum of a Geometric Series
• 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

Theorems 79 to 100

• 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
• 99. Buffon Needle Problem
• 100. Descartes Rule of Signs

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.