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 a rule 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.

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 Coninuum 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 Thoerem	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 Trancendental	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 Bernouilli	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