Freek Wiedijk’s “Formalizing 100 Theorems” list is a long-standing benchmark for interactive theorem provers. It catalogs 100 significant mathematical results drawn from across pure mathematics — number theory, analysis, algebra, combinatorics, and geometry — and tracks which provers have successfully formalized each one. Mathlib has formalized a large share of these theorems, with declarations spread across its module hierarchy and tracked in the repository fileDocumentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover-community/mathlib4/llms.txt
Use this file to discover all available pages before exploring further.
docs/100.yaml. That file records the canonical Lean 4 declaration name, the contributing authors, and links to any external-repository proofs for theorems that live outside Mathlib proper.
About the Benchmark
Wiedijk’s list was designed to include theorems that are mathematically non-trivial, span many areas of mathematics, and were historically important — not merely technically hard to formalize. A theorem prover that covers the full list demonstrates breadth and robustness in its mathematical library. Mathlib aims for completeness and continuously adds new entries as contributors formalize remaining items.Some of the 100 theorems have been formalized in external projects (separate GitHub repositories) rather than in Mathlib itself. The
docs/100.yaml file links to those proofs where applicable. The lake exe check-yaml command verifies that all declaration names in the YAML file exist in the current build.Formalized Theorems by Area
The theorems below are drawn directly fromdocs/100.yaml. Each entry shows the theorem number, its title, the Lean 4 declaration name(s), and the primary author(s).
Number Theory and Arithmetic
Theorems 1, 10, 11, 19, 20, 48, 51, 80, 81, 98
Theorems 1, 10, 11, 19, 20, 48, 51, 80, 81, 98
#1 — The Irrationality of the Square Root of 2Authors: mathlib#10 — Euler’s Generalization of Fermat’s Little TheoremAuthors: Chris Hughes#11 — The Infinitude of PrimesAuthors: Jeremy Avigad#19 — Four Squares TheoremAuthors: Chris Hughes#20 — All Primes (1 mod 4) Equal the Sum of Two SquaresAuthors: Chris Hughes#48 — Dirichlet’s Theorem on Primes in Arithmetic ProgressionsAuthors: David Loeffler, Michael Stoll#51 — Wilson’s LemmaAuthors: Chris Hughes#80 — The Fundamental Theorem of ArithmeticAuthors: Chris Hughes — also proved in generality: every Euclidean domain is a unique factorization domain, and Authors: Manuel Candales (archive), Michael Stoll (mathlib)#98 — Bertrand’s PostulateAuthors: Bolton Bailey, Patrick Stevens
Int is a Euclidean domain (Int.euclideanDomain).#81 — Divergence of the Prime Reciprocal SeriesAnalysis and Calculus
Theorems 14, 15, 26, 34, 35, 38, 64, 75, 76, 79, 86, 90, 91
Theorems 14, 15, 26, 34, 35, 38, 64, 75, 76, 79, 86, 90, 91
#14 — Euler’s Summation of 1 + (1/2)² + (1/3)² + …Authors: Marc Masdeu, David Loeffler#15 — Fundamental Theorem of Integral CalculusAuthors: Yury G. Kudryashov (first form), Benjamin Davidson (second form)#26 — Leibniz’s Series for PiAuthors: Benjamin Davidson#34 — Divergence of the Harmonic SeriesAuthors: Anatole Dedecker, Yury Kudryashov#35 — Taylor’s TheoremAuthors: Moritz Doll#38 — Arithmetic Mean / Geometric Mean InequalityAuthors: Yury G. Kudryashov#64 — L’Hôpital’s RuleAuthors: Anatole Dedecker#75 — The Mean Value TheoremAuthors: Yury G. Kudryashov#76 — Fourier SeriesAuthors: Heather Macbeth#79 — The Intermediate Value TheoremAuthors: Rob Lewis, Chris Hughes#86 — Lebesgue Measure and IntegrationAuthors: Johannes Hölzl#90 — Stirling’s FormulaAuthors: Moritz Firsching, Fabian Kruse, Nikolas Kuhn, Heather Macbeth#91 — The Triangle InequalityAuthors: Zhouhang Zhou
Algebra
Theorems 2, 7, 16, 17, 18, 37, 39, 44, 46, 49, 71, 72, 89
Theorems 2, 7, 16, 17, 18, 37, 39, 44, 46, 49, 71, 72, 89
#2 — Fundamental Theorem of AlgebraAuthors: Chris Hughes#7 — Law of Quadratic ReciprocityAuthors: Chris Hughes (Legendre symbol), Michael Stoll (Jacobi symbol)#16 — Insolvability of General Higher Degree Equations (Abel–Ruffini Theorem)Authors: Thomas Browning#17 — De Moivre’s FormulaAuthors: Abhimanyu Pallavi Sudhir#18 — Liouville’s Theorem and the Construction of Transcendental NumbersAuthors: Jujian Zhang#37 — The Solution of a CubicAuthors: Jeoff Lee#39 — Solutions to Pell’s EquationAuthors: Mario Carneiro (first), Michael Stoll (second)#44 — The Binomial TheoremAuthors: Chris Hughes#46 — The Solution of the General Quartic EquationAuthors: Thomas Zhu#49 — The Cayley–Hamilton TheoremAuthors: Kim Morrison#71 — Order of a Subgroup (Lagrange’s Theorem)Authors: mathlib#72 — Sylow’s TheoremAuthors: Chris Hughes#89 — The Factor and Remainder TheoremsAuthors: Chris Hughes
Geometry
Theorems 4, 9, 27, 40, 55, 57, 61, 65, 94, 95
Theorems 4, 9, 27, 40, 55, 57, 61, 65, 94, 95
#4 — Pythagorean TheoremAuthors: Joseph Myers#9 — The Area of a CircleAuthors: James Arthur, Benjamin Davidson, Andrew Souther#27 — Sum of the Angles of a TriangleAuthors: Joseph Myers#40 — Minkowski’s Fundamental TheoremAuthors: Alex J. Best, Yaël Dillies#55 — Product of Segments of ChordsAuthors: Manuel Candales#57 — Heron’s FormulaAuthors: Matt Kempster#61 — Theorem of CevaAuthors: Joseph Myers#65 — Isosceles Triangle TheoremAuthors: Joseph Myers#94 — The Law of CosinesAuthors: Joseph Myers#95 — Ptolemy’s TheoremAuthors: Manuel Candales
Combinatorics and Probability
Theorems 30, 47, 52, 58, 59, 62, 63, 73, 78, 83, 88, 93, 96
Theorems 30, 47, 52, 58, 59, 62, 63, 73, 78, 83, 88, 93, 96
#30 — The Ballot ProblemAuthors: Bhavik Mehta, Kexing Ying#47 — The Central Limit TheoremAuthors: Thomas Zhu, Rémy Degenne, Etienne Marion#52 — The Number of Subsets of a SetAuthors: mathlib#58 — Formula for the Number of CombinationsAuthors: mathlib#59 — The Laws of Large NumbersAuthors: Sébastien Gouëzel#62 — Fair Games Theorem (Optional Stopping)Authors: Kexing Ying#63 — Cantor’s TheoremAuthors: Johannes Hölzl, Mario Carneiro#73 — Ascending or Descending Sequences (Erdős–Szekeres Theorem)Authors: Bhavik Mehta#78 — The Cauchy–Schwarz InequalityAuthors: Zhouhang Zhou#83 — The Friendship TheoremAuthors: Aaron Anderson, Jalex Stark, Kyle Miller#88 — Derangements FormulaAuthors: Henry Swanson#93 — The Birthday ProblemAuthors: Eric Rodriguez#96 — Principle of Inclusion/ExclusionAuthors: Neil Strickland (outside mathlib), Yaël Dillies (in mathlib)
Further Notable Entries
Theorems 3, 22, 23, 25, 42, 45, 54, 60, 66, 68, 69, 70, 74, 77, 82, 85, 97, 99, 100
Theorems 3, 22, 23, 25, 42, 45, 54, 60, 66, 68, 69, 70, 74, 77, 82, 85, 97, 99, 100
#3 — The Denumerability of the Rational NumbersAuthors: Chris Hughes#22 — The Non-Denumerability of the ContinuumAuthors: Floris van Doorn#23 — Formula for Pythagorean TriplesAuthors: Paul van Wamelen#25 — Schroeder–Bernstein TheoremAuthors: Mario Carneiro#42 — Sum of the Reciprocals of the Triangular NumbersAuthors: Jalex Stark, Yury Kudryashov#45 — The Partition TheoremAuthors: Bhavik Mehta, Aaron Anderson, Weiyi Wang#54 — Königsberg Bridges ProblemAuthors: Kyle Miller#60 — Bézout’s TheoremAuthors: mathlib#66 — Sum of a Geometric SeriesAuthors: Sander R. Dahmen (finite), Johannes Hölzl (infinite)#68 — Sum of an Arithmetic SeriesAuthors: Johannes Hölzl#69 — Greatest Common Divisor AlgorithmAuthors: mathlib#70 — The Perfect Number TheoremAuthors: Aaron Anderson#74 — The Principle of Mathematical InductionNote: automatically generated when defining the natural numbers. Authors: Leonardo de Moura#77 — Sum of kth PowersAuthors: Moritz Firsching, Fabian Kruse, Ashvni Narayanan#82 — Dissection of Cubes (Littlewood’s elegant proof)Authors: Floris van Doorn#85 — Divisibility by 3 RuleAuthors: Kim Morrison#97 — Cramer’s RuleAuthors: Anne Baanen#99 — Buffon Needle ProblemAuthors: Enrico Z. Borba#100 — Descartes’ Rule of SignsAuthors: Alex Meiburg
Ongoing and External Proofs
Several entries on the list have been formalized in dedicated external repositories rather than Mathlib proper. These include:- #5 (Prime Number Theorem) — Alex Kontorovich, Terry Tao, et al. in the PrimeNumberTheoremAnd project.
- #6 (Gödel’s Incompleteness Theorem) — Shogo Saito in FormalizedFormalLogic/Foundation.
- #24 (Independence of the Continuum Hypothesis) — Jesse Michael Han and Floris van Doorn in the flypitch project.
- #31 (Ramsey’s Theorem) — Bhavik Mehta in a separate combinatorics repository.
- #33 (Fermat’s Last Theorem) — ongoing formalization at imperialcollegelondon.github.io/FLT.
- #36 (Brouwer Fixed Point Theorem) — Brendan Seamas Murphy in Shamrock-Frost/BrouwerFixedPoint.
- #67 (e is Transcendental) — Jujian Zhang in a dedicated transcendental numbers repository.