From 3fbeb2bc98307b9c622505c48726fce50a6e6e0a Mon Sep 17 00:00:00 2001 From: Ken Monks Date: Sun, 1 Dec 2024 21:31:45 -0800 Subject: [PATCH] Fixing relative paths for forked sites. --- 100/index.html | 1774 +++++++++++++++++++++--------------------- index.html | 2023 +++++++++++++++--------------------------------- 2 files changed, 1508 insertions(+), 2289 deletions(-) diff --git a/100/index.html b/100/index.html index d880d450..6ce717ee 100644 --- a/100/index.html +++ b/100/index.html @@ -1,934 +1,900 @@ - + + - - - - 100 Theorems! - - - - - + + 100 Theorems! + + + + + + + + - - + + - - + - - + - - -
- - -
-
- Ken Monks -
-
- monks.scranton.edu -
-
- proveitmath.org -
+ + + + - -
-
-
-

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

-
-
-

- Status: ✔︎ 1 proof verified, - ? 99 unverified -

-
+ +
+ +
+
+

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

+
+
+

Status: ✔︎ 1 proof verified, ? 99 unverified

+
+
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
Done#TheoremAuthorDate
✔︎1The Irrationality of the Square Root of 2Pythagoras and his school500 B.C.
?2Fundamental Theorem of AlgebraKarl Frederich Gauss1799
?3The Denumerability of the Rational NumbersGeorg Cantor1867
?4Pythagorean TheoremPythagoras and his school500 B.C.
?5Prime Number Theorem +
Jacques Hadamard and Charles-Jean de la Vallee Poussin + (separately)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Done#TheoremAuthorDate
✔︎1The Irrationality of the Square Root of 2Pythagoras and his school500 B.C.
?2Fundamental Theorem of AlgebraKarl Frederich Gauss1799
?3The Denumerability of the Rational NumbersGeorg Cantor1867
?4Pythagorean TheoremPythagoras and his school500 B.C.
?5Prime Number Theorem -
- Jacques Hadamard and Charles-Jean de la Vallee Poussin - (separately) -
- 		1896
?6Godel’s Incompleteness TheoremKurt Godel1931
?7Law of Quadratic ReciprocityKarl Frederich Gauss1801
?8 - The Impossibility of Trisecting the Angle and Doubling the Cube - Pierre Wantzel1837
?9The Area of a CircleArchimedes225 B.C.
?10 - Euler’s Generalization of Fermat’s Little Theorem
(Fermat’s - Little Theorem) - 		Leonhard Euler
(Pierre de Fermat)		1760
(1640)
?11The Infinitude of PrimesEuclid300 B.C.
?12The Independence of the Parallel Postulate - Karl Frederich Gauss, Janos Bolyai, Nikolai Lobachevsky, G.F. - Bernhard Riemann collectively - 1870-1880
?13Polyhedron FormulaLeonhard Euler1751
?14Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….Leonhard Euler1734
?15Fundamental Theorem of Integral CalculusGottfried Wilhelm von Leibniz1686
?16Insolvability of General Higher Degree EquationsNiels Henrik Abel1824
?17DeMoivre’s TheoremAbraham DeMoivre1730
?18 - Liouville’s Theorem and the Construction of Trancendental - Numbers - Joseph Liouville1844
?19Four Squares TheoremJoseph-Louis Lagrange1770
?20All Primes Equal the Sum of Two Squares??
?21Green’s TheoremGeorge Green1828
?22The Non-Denumerability of the ContinuumGeorg Cantor1874
?23Formula for Pythagorean TriplesEuclid300 B.C.
?24The Undecidability of the Coninuum HypothesisPaul Cohen1963
?25Schroeder-Bernstein Theorem??
?26Leibnitz’s Series for PiGottfried Wilhelm von Leibniz1674
?27Sum of the Angles of a TriangleEuclid300 B.C.
?28Pascal’s Hexagon TheoremBlaise Pascal1640
?29Feuerbach’s TheoremKarl Wilhelm Feuerbach1822
?30The Ballot ProblemJ.L.F. Bertrand1887
?31Ramsey’s TheoremF.P. Ramsey1930
?32The Four Color ProblemKenneth Appel and Wolfgang Haken1976
?33Fermat’s Last TheoremAndrew Wiles1993
?34Divergence of the Harmonic SeriesNicole Oresme1350
?35Taylor’s TheoremBrook Taylor1715
?36Brouwer Fixed Point TheoremL.E.J. Brouwer1910
?37The Solution of a CubicScipione Del Ferro1500
?38 - Arithmetic Mean/Geometric Mean
(Proof by Backward - Induction)
(Polya Proof) -
Augustin-Louis Cauchy
George Polya
?
?
?39Solutions to Pell’s EquationLeonhard Euler1759
?40Minkowski’s Fundamental TheoremHermann Minkowski1896
?41Puiseux’s Theorem - Victor Puiseux (based on a discovery of Isaac Newton of 1671) - 1850
?42Sum of the Reciprocals of the Triangular NumbersGottfried Wilhelm von Leibniz1672
?43The Isoperimetric TheoremJacob Steiner1838
?44The Binomial TheoremIsaac Newton1665
?45The Partition TheoremLeonhard Euler1740
?46The Solution of the General Quartic EquationLodovico Ferrari1545
?47The Central Limit Theorem??
?48Dirichlet’s TheoremPeter Lejune Dirichlet1837
?49The Cayley-Hamilton ThoeremArthur Cayley1858
?50The Number of Platonic SolidsTheaetetus400 B.C.
?51Wilson’s TheoremJoseph-Louis Lagrange1773
?52The Number of Subsets of a Set??
?53Pi is TrancendentalFerdinand Lindemann1882
?54Konigsberg Bridges ProblemLeonhard Euler1736
?55Product of Segments of ChordsEuclid300 B.C.
?56The Hermite-Lindemann Transcendence TheoremFerdinand Lindemann1882
?57Heron’s FormulaHeron of Alexandria75
?58Formula for the Number of Combinations??
?59The Laws of Large Numbers<many><many>
?60Bezout’s TheoremEtienne Bezout?
?61Theorem of CevaGiovanni Ceva1678
?62Fair Games Theorem??
?63Cantor’s TheoremGeorg Cantor1891
?64L’Hopital’s RuleJohn Bernoulli1696?
?65Isosceles Triangle TheoremEuclid300 B.C.
?66Sum of a Geometric SeriesArchimedes260 B.C.?
?67e is TranscendentalCharles Hermite1873
?68Sum of an arithmetic seriesBabylonians1700 B.C.
?69Greatest Common Divisor AlgorithmEuclid300 B.C.
?70The Perfect Number TheoremEuclid300 B.C.
?71Order of a SubgroupJoseph-Louis Lagrange1802
?72Sylow’s TheoremLudwig Sylow1870
?73Ascending or Descending SequencesPaul Erdos and G. Szekeres1935
?74The Principle of Mathematical InductionLevi ben Gerson1321
?75The Mean Value TheoremAugustine-Louis Cauchy1823
?76Fourier SeriesJoseph Fourier1811
?77Sum of kth powersJakob Bernouilli1713
?78The Cauchy-Schwarz InequalityAugustine-Louis Cauchy1814?
?79The Intermediate Value TheoremAugustine-Louis Cauchy1821
?80The Fundamental Theorem of ArithmeticEuclid300 B.C.
?81Divergence of the Prime Reciprocal SeriesLeonhard Euler1734?
?82Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)R.L. Brooks1940
?83The Friendship TheoremPaul Erdos, Alfred Renyi, Vera Sos1966
?84Morley’s TheoremFrank Morley1899
?85Divisibility by 3 Rule??
?86Lebesgue Measure and IntegrationHenri Lebesgue1902
?87Desargues’s TheoremGerard Desargues1650
?88Derangements Formula??
?89The Factor and Remainder Theorems??
?90Stirling’s FormulaJames Stirling1730
?91The Triangle Inequality??
?92Pick’s TheoremGeorge Pick1899
?93The Birthday Problem??
?94The Law of CosinesFrancois Viete1579
?95Ptolemy’s TheoremPtolemy120?
?96Principle of Inclusion/Exclusion??
?97Cramer’s RuleGabriel Cramer1750
?98Bertrand’s PostulateJ.L.F. Bertrand1860?
?99Buffon Needle ProblemComte de Buffon1733
?100Descartes Rule of SignsRene Descartes1637
- + 		1896
?6Godel’s Incompleteness TheoremKurt Godel1931
?7Law of Quadratic ReciprocityKarl Frederich Gauss1801
?8The Impossibility of Trisecting the Angle and Doubling the + CubePierre Wantzel1837
?9The Area of a CircleArchimedes225 B.C.
?10Euler’s Generalization of Fermat’s Little + Theorem
(Fermat’s Little + Theorem)		Leonhard Euler
(Pierre de Fermat)		1760
(1640)
?11The Infinitude of PrimesEuclid300 B.C.
?12The Independence of the Parallel PostulateKarl Frederich Gauss, Janos Bolyai, Nikolai Lobachevsky, + G.F. Bernhard + Riemann collectively1870-1880
?13Polyhedron FormulaLeonhard Euler1751
?14Euler’s Summation of 1 + (1/2)^2 + (1/3)^2 + ….Leonhard Euler1734
?15Fundamental Theorem of Integral CalculusGottfried Wilhelm von Leibniz1686
?16Insolvability of General Higher Degree EquationsNiels Henrik Abel1824
?17DeMoivre’s TheoremAbraham DeMoivre1730
?18Liouville’s Theorem and the Construction of Trancendental + NumbersJoseph Liouville1844
?19Four Squares TheoremJoseph-Louis Lagrange1770
?20All Primes Equal the Sum of Two Squares??
?21Green’s TheoremGeorge Green1828
?22The Non-Denumerability of the ContinuumGeorg Cantor1874
?23Formula for Pythagorean TriplesEuclid300 B.C.
?24The Undecidability of the Coninuum HypothesisPaul Cohen1963
?25Schroeder-Bernstein Theorem??
?26Leibnitz’s Series for PiGottfried Wilhelm von Leibniz1674
?27Sum of the Angles of a TriangleEuclid300 B.C.
?28Pascal’s Hexagon TheoremBlaise Pascal1640
?29Feuerbach’s TheoremKarl Wilhelm Feuerbach1822
?30The Ballot ProblemJ.L.F. Bertrand1887
?31Ramsey’s TheoremF.P. Ramsey1930
?32The Four Color ProblemKenneth Appel and Wolfgang Haken1976
?33Fermat’s Last TheoremAndrew Wiles1993
?34Divergence of the Harmonic SeriesNicole Oresme1350
?35Taylor’s TheoremBrook Taylor1715
?36Brouwer Fixed Point TheoremL.E.J. Brouwer1910
?37The Solution of a CubicScipione Del Ferro1500
?38Arithmetic Mean/Geometric Mean
(Proof by Backward + Induction)
(Polya Proof)
Augustin-Louis Cauchy
George Polya
?
?
?39Solutions to Pell’s EquationLeonhard Euler1759
?40Minkowski’s Fundamental TheoremHermann Minkowski1896
?41Puiseux’s TheoremVictor Puiseux (based on a discovery of Isaac Newton of + 1671)1850
?42Sum of the Reciprocals of the Triangular NumbersGottfried Wilhelm von Leibniz1672
?43The Isoperimetric TheoremJacob Steiner1838
?44The Binomial TheoremIsaac Newton1665
?45The Partition TheoremLeonhard Euler1740
?46The Solution of the General Quartic EquationLodovico Ferrari1545
?47The Central Limit Theorem??
?48Dirichlet’s TheoremPeter Lejune Dirichlet1837
?49The Cayley-Hamilton ThoeremArthur Cayley1858
?50The Number of Platonic SolidsTheaetetus400 B.C.
?51Wilson’s TheoremJoseph-Louis Lagrange1773
?52The Number of Subsets of a Set??
?53Pi is TrancendentalFerdinand Lindemann1882
?54Konigsberg Bridges ProblemLeonhard Euler1736
?55Product of Segments of ChordsEuclid300 B.C.
?56The Hermite-Lindemann Transcendence TheoremFerdinand Lindemann1882
?57Heron’s FormulaHeron of Alexandria75
?58Formula for the Number of Combinations??
?59The Laws of Large Numbers<many><many>
?60Bezout’s TheoremEtienne Bezout?
?61Theorem of CevaGiovanni Ceva1678
?62Fair Games Theorem??
?63Cantor’s TheoremGeorg Cantor1891
?64L’Hopital’s RuleJohn Bernoulli1696?
?65Isosceles Triangle TheoremEuclid300 B.C.
?66Sum of a Geometric SeriesArchimedes260 B.C.?
?67e is TranscendentalCharles Hermite1873
?68Sum of an arithmetic seriesBabylonians1700 B.C.
?69Greatest Common Divisor AlgorithmEuclid300 B.C.
?70The Perfect Number TheoremEuclid300 B.C.
?71Order of a SubgroupJoseph-Louis Lagrange1802
?72Sylow’s TheoremLudwig Sylow1870
?73Ascending or Descending SequencesPaul Erdos and G. Szekeres1935
?74The Principle of Mathematical InductionLevi ben Gerson1321
?75The Mean Value TheoremAugustine-Louis Cauchy1823
?76Fourier SeriesJoseph Fourier1811
?77Sum of kth powersJakob Bernouilli1713
?78The Cauchy-Schwarz InequalityAugustine-Louis Cauchy1814?
?79The Intermediate Value TheoremAugustine-Louis Cauchy1821
?80The Fundamental Theorem of ArithmeticEuclid300 B.C.
?81Divergence of the Prime Reciprocal SeriesLeonhard Euler1734?
?82Dissection of Cubes (J.E. Littlewood’s ‘elegant’ proof)R.L. Brooks1940
?83The Friendship TheoremPaul Erdos, Alfred Renyi, Vera Sos1966
?84Morley’s TheoremFrank Morley1899
?85Divisibility by 3 Rule??
?86Lebesgue Measure and IntegrationHenri Lebesgue1902
?87Desargues’s TheoremGerard Desargues1650
?88Derangements Formula??
?89The Factor and Remainder Theorems??
?90Stirling’s FormulaJames Stirling1730
?91The Triangle Inequality??
?92Pick’s TheoremGeorge Pick1899
?93The Birthday Problem??
?94The Law of CosinesFrancois Viete1579
?95Ptolemy’s TheoremPtolemy120?
?96Principle of Inclusion/Exclusion??
?97Cramer’s RuleGabriel Cramer1750
?98Bertrand’s PostulateJ.L.F. Bertrand1860?
?99Buffon Needle ProblemComte de Buffon1733
?100Descartes Rule of SignsRene Descartes1637
+ +
-