Ken Monks
monks.scranton.edu
proveitmath.org
github.com/kenmonks/lurch

100 Theorems in Lurch

Freek Wiedijk maintains a list tracking progress of theorem provers formalizing 100 classic theorems in mathematics. On this page we collect all of the proofs on that list that we have formalized in Lurch to date.

Since Lurch supports proofs in any context, deciding what actually constitutes a formalization of one of the proofs is not obvious. For example, one can simply add each of the 100 theorems to the context of a Lurch document as rules and they will all be 'proven' trivially.

To address this, we self-impose our own standard for what qualifies. Consistent with Lurch's philosophy, we consider a theorem to be proved by Lurch if the proof contains, at minimum, the level of detail you might find for the proof of that theorem in a textbook, spotting all of the other details as part of the context. Citing a proof of the theorem in a textbook or other valid source can certify that this criteria has been met.

100 Theorem Checklist

The following table is reproduced from here (if there is a newer version of that page let me know). A green check mark () in the first column indicates that Lurch has proved the theorem listed, while a yellow question mark () indicates that it has not.

Click on a completed theorem to open its proof in Lurch.

Status: 2 proofs verified, 98 unverified

Done # Theorem Author Date
1 The Irrationality of the Square Root of 2 Pythagoras and his school 500 B.C.
2 Fundamental Theorem of Algebra Karl Frederich Gauss 1799
3 The Denumerability of the Rational Numbers Georg Cantor 1867
4 Pythagorean Theorem Pythagoras and his school 500 B.C.
5 Prime Number Theorem
Jacques Hadamard and Charles-Jean de la Vallee Poussin (separately)
1896
6 Godel’s Incompleteness Theorem Kurt Godel 1931
7 Law of Quadratic Reciprocity Karl Frederich Gauss 1801
8 The Impossibility of Trisecting the Angle and Doubling the Cube Pierre Wantzel 1837
9 The Area of a Circle Archimedes 225 B.C.
10 Euler’s Generalization of Fermat’s Little Theorem
(Fermat’s Little Theorem)		 Leonhard Euler
(Pierre de Fermat)		 1760
(1640)
11 The Infinitude of Primes Euclid 300 B.C.
12 The Independence of the Parallel Postulate Karl Frederich Gauss, Janos Bolyai, Nikolai Lobachevsky, G.F. Bernhard Riemann collectively 1870-1880
13 Polyhedron Formula Leonhard Euler 1751
14 Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + …. Leonhard Euler 1734
15 Fundamental Theorem of Integral Calculus Gottfried Wilhelm von Leibniz 1686
16 Insolvability of General Higher Degree Equations Niels Henrik Abel 1824
17 DeMoivre’s Theorem Abraham DeMoivre 1730
18 Liouville’s Theorem and the Construction of Trancendental Numbers Joseph Liouville 1844
19 Four Squares Theorem Joseph-Louis Lagrange 1770
20 All Primes Equal the Sum of Two Squares ? ?
21 Green’s Theorem George Green 1828
22 The Non-Denumerability of the Continuum Georg Cantor 1874
23 Formula for Pythagorean Triples Euclid 300 B.C.
24 The Undecidability of the Continuum Hypothesis Paul Cohen 1963
25 Schroeder-Bernstein Theorem ? ?
26 Leibnitz’s Series for Pi Gottfried Wilhelm von Leibniz 1674
27 Sum of the Angles of a Triangle Euclid 300 B.C.
28 Pascal’s Hexagon Theorem Blaise Pascal 1640
29 Feuerbach’s Theorem Karl Wilhelm Feuerbach 1822
30 The Ballot Problem J.L.F. Bertrand 1887
31 Ramsey’s Theorem F.P. Ramsey 1930
32 The Four Color Problem Kenneth Appel and Wolfgang Haken 1976
33 Fermat’s Last Theorem Andrew Wiles 1993
34 Divergence of the Harmonic Series Nicole Oresme 1350
35 Taylor’s Theorem Brook Taylor 1715
36 Brouwer Fixed Point Theorem L.E.J. Brouwer 1910
37 The Solution of a Cubic Scipione Del Ferro 1500
38 Arithmetic Mean/Geometric Mean
(Proof by Backward Induction)
(Polya Proof)
Augustin-Louis Cauchy
George Polya
?
?
39 Solutions to Pell’s Equation Leonhard Euler 1759
40 Minkowski’s Fundamental Theorem Hermann Minkowski 1896
41 Puiseux’s Theorem Victor Puiseux (based on a discovery of Isaac Newton of 1671) 1850
42 Sum of the Reciprocals of the Triangular Numbers Gottfried Wilhelm von Leibniz 1672
43 The Isoperimetric Theorem Jacob Steiner 1838
44 The Binomial Theorem Isaac Newton 1665
45 The Partition Theorem Leonhard Euler 1740
46 The Solution of the General Quartic Equation Lodovico Ferrari 1545
47 The Central Limit Theorem ? ?
48 Dirichlet’s Theorem Peter Lejune Dirichlet 1837
49 The Cayley-Hamilton Theorem Arthur Cayley 1858
50 The Number of Platonic Solids Theaetetus 400 B.C.
51 Wilson’s Theorem Joseph-Louis Lagrange 1773
52 The Number of Subsets of a Set ? ?
53 Pi is Transcendental Ferdinand Lindemann 1882
54 Konigsberg Bridges Problem Leonhard Euler 1736
55 Product of Segments of Chords Euclid 300 B.C.
56 The Hermite-Lindemann Transcendence Theorem Ferdinand Lindemann 1882
57 Heron’s Formula Heron of Alexandria 75
58 Formula for the Number of Combinations ? ?
59 The Laws of Large Numbers <many> <many>
60 Bezout’s Theorem Etienne Bezout ?
61 Theorem of Ceva Giovanni Ceva 1678
62 Fair Games Theorem ? ?
63 Cantor’s Theorem Georg Cantor 1891
64 L’Hopital’s Rule John Bernoulli 1696?
65 Isosceles Triangle Theorem Euclid 300 B.C.
66 Sum of a Geometric Series Archimedes 260 B.C.?
67 e is Transcendental Charles Hermite 1873
68 Sum of an arithmetic series Babylonians 1700 B.C.
69 Greatest Common Divisor Algorithm Euclid 300 B.C.
70 The Perfect Number Theorem Euclid 300 B.C.
71 Order of a Subgroup Joseph-Louis Lagrange 1802
72 Sylow’s Theorem Ludwig Sylow 1870
73 Ascending or Descending Sequences Paul Erdos and G. Szekeres 1935
74 The Principle of Mathematical Induction Levi ben Gerson 1321
75 The Mean Value Theorem Augustine-Louis Cauchy 1823
76 Fourier Series Joseph Fourier 1811
77 Sum of kth powers Jakob Bernoulli 1713
78 The Cauchy-Schwarz Inequality Augustine-Louis Cauchy 1814?
79 The Intermediate Value Theorem Augustine-Louis Cauchy 1821
80 The Fundamental Theorem of Arithmetic Euclid 300 B.C.
81 Divergence of the Prime Reciprocal Series Leonhard Euler 1734?
82 Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof) R.L. Brooks 1940
83 The Friendship Theorem Paul Erdos, Alfred Renyi, Vera Sos 1966
84 Morley’s Theorem Frank Morley 1899
85 Divisibility by 3 Rule ? ?
86 Lebesgue Measure and Integration Henri Lebesgue 1902
87 Desargues’s Theorem Gerard Desargues 1650
88 Derangements Formula ? ?
89 The Factor and Remainder Theorems ? ?
90 Stirling’s Formula James Stirling 1730
91 The Triangle Inequality ? ?
92 Pick’s Theorem George Pick 1899
93 The Birthday Problem ? ?
94 The Law of Cosines Francois Viete 1579
95 Ptolemy’s Theorem Ptolemy 120?
96 Principle of Inclusion/Exclusion ? ?
97 Cramer’s Rule Gabriel Cramer 1750
98 Bertrand’s Postulate J.L.F. Bertrand 1860?
99 Buffon Needle Problem Comte de Buffon 1733
100 Descartes Rule of Signs Rene Descartes 1637