Mathelia Books for Freek Wiedijk's list of 100 theorems, written by an AI (Claude): 22 so far. Each link opens the Book; no account is needed. Several theorems have more than one Book, with different constructions or proofs. Systems is the number of formal systems (HOL Light, Isabelle, Lean, Metamath, …) listed on Freek's page as having formalized the theorem, as of 2026-10-16.
| No. | Theorem | Mathelia | Systems |
|---|---|---|---|
| 1 | The Irrationality of the Square Root of 2 | [1] | 13 |
| 2 | Fundamental Theorem of Algebra | 9 | |
| 3 | The Denumerability of the Rational Numbers | [3] [3b] | 12 |
| 4 | Pythagorean Theorem | 9 | |
| 5 | Prime Number Theorem | 4 | |
| 6 | Gödel's Incompleteness Theorem | 5 | |
| 7 | Law of Quadratic Reciprocity | 7 | |
| 8 | The Impossibility of Trisecting the Angle and Doubling the Cube | 2 | |
| 9 | The Area of a Circle | 6 | |
| 10 | Euler's Generalization of Fermat's Little Theorem | [10] (prime case only) | 7 |
| 11 | The Infinitude of Primes | [11] [11b] | 12 |
| 12 | The Independence of the Parallel Postulate | 2 | |
| 13 | Polyhedron Formula | 4 | |
| 14 | Euler's Summation of 1 + (1/2)^2 + (1/3)^2 + .... | 6 | |
| 15 | Fundamental Theorem of Integral Calculus | 9 | |
| 16 | Insolvability of General Higher Degree Equations | 2 | |
| 17 | De Moivre's Theorem | 8 | |
| 18 | Liouville's Theorem and the Construction of Transcendental Numbers | 6 | |
| 19 | Four Squares Theorem | 8 | |
| 20 | All Primes (1 mod 4) Equal the Sum of Two Squares | 9 | |
| 21 | Green's Theorem | 2 | |
| 22 | The Non-Denumerability of the Continuum | 10 | |
| 23 | Formula for Pythagorean Triples | [23] | 8 |
| 24 | The Undecidability of the Continuum Hypothesis | 2 | |
| 25 | Schroeder-Bernstein Theorem | [25] | 10 |
| 26 | Leibniz's Series for Pi | 7 | |
| 27 | Sum of the Angles of a Triangle | 6 | |
| 28 | Pascal's Hexagon Theorem | 3 | |
| 29 | Feuerbach's Theorem | 3 | |
| 30 | The Ballot Problem | 8 | |
| 31 | Ramsey's Theorem | [31] | 11 |
| 32 | The Four Color Problem | 1 | |
| 33 | Fermat's Last Theorem | 1 | |
| 34 | Divergence of the Harmonic Series | 10 | |
| 35 | Taylor's Theorem | 9 | |
| 36 | Brouwer Fixed Point Theorem | 4 | |
| 37 | The Solution of a Cubic | 6 | |
| 38 | Arithmetic Mean/Geometric Mean | 8 | |
| 39 | Solutions to Pell's Equation | 5 | |
| 40 | Minkowski's Fundamental Theorem | 4 | |
| 41 | Puiseux's Theorem | 2 | |
| 42 | Sum of the Reciprocals of the Triangular Numbers | 9 | |
| 43 | The Isoperimetric Theorem | 1 | |
| 44 | The Binomial Theorem | [44] | 10 |
| 45 | The Partition Theorem | 6 | |
| 46 | The Solution of the General Quartic Equation | 6 | |
| 47 | The Central Limit Theorem | 2 | |
| 48 | Dirichlet's Theorem | 4 | |
| 49 | The Cayley-Hamilton Theorem | 5 | |
| 50 | The Number of Platonic Solids | 2 | |
| 51 | Wilson's Theorem | [51] | 8 |
| 52 | The Number of Subsets of a Set | [52a] [52b] | 11 |
| 53 | Pi is Transcendental | 3 | |
| 54 | Konigsberg Bridges Problem | 8 | |
| 55 | Product of Segments of Chords | 6 | |
| 56 | The Hermite-Lindemann Transcendence Theorem | 3 | |
| 57 | Heron's Formula | 6 | |
| 58 | Formula for the Number of Combinations | [58a] [58b] | 9 |
| 59 | The Laws of Large Numbers | 4 | |
| 60 | Bezout's Theorem | [60] [60b] | 12 |
| 61 | Theorem of Ceva | 5 | |
| 62 | Fair Games Theorem | 4 | |
| 63 | Cantor's Theorem | [63] | 11 |
| 64 | L'Hôpital's Rule | 7 | |
| 65 | Isosceles Triangle Theorem | 7 | |
| 66 | Sum of a Geometric Series | [66] | 11 |
| 67 | e is Transcendental | 6 | |
| 68 | Sum of an arithmetic series | [68a] [68b] | 11 |
| 69 | Greatest Common Divisor Algorithm | [69] [69b] | 13 |
| 70 | The Perfect Number Theorem | 7 | |
| 71 | Order of a Subgroup | 9 | |
| 72 | Sylow's Theorem | 8 | |
| 73 | Ascending or Descending Sequences | [73] | 7 |
| 74 | The Principle of Mathematical Induction | [74a] [74b] | 11 |
| 75 | The Mean Value Theorem | 9 | |
| 76 | Fourier Series | 4 | |
| 77 | Sum of kth powers | 5 | |
| 78 | The Cauchy-Schwarz Inequality | 10 | |
| 79 | The Intermediate Value Theorem | 9 | |
| 80 | The Fundamental Theorem of Arithmetic | [80] | 12 |
| 81 | Divergence of the Prime Reciprocal Series | 8 | |
| 82 | Dissection of Cubes (J.E. Littlewood's "elegant" proof) | 3 | |
| 83 | The Friendship Theorem | 6 | |
| 84 | Morley's Theorem | 4 | |
| 85 | Divisibility by 3 Rule | [85] | 10 |
| 86 | Lebesgue Measure and Integration | 6 | |
| 87 | Desargues's Theorem | 5 | |
| 88 | Derangements Formula | [88a] [88b] [88c] | 7 |
| 89 | The Factor and Remainder Theorems | 7 | |
| 90 | Stirling's Formula | 5 | |
| 91 | The Triangle Inequality | 10 | |
| 92 | Pick's Theorem | 2 | |
| 93 | The Birthday Problem | 8 | |
| 94 | The Law of Cosines | 7 | |
| 95 | Ptolemy's Theorem | 6 | |
| 96 | Principle of Inclusion/Exclusion | [96] [96b] | 9 |
| 97 | Cramer's Rule | 7 | |
| 98 | Bertrand's Postulate | 6 | |
| 99 | Buffon Needle Problem | 4 | |
| 100 | Descartes Rule of Signs | 4 |