+- MKLab (https://mklab.gr)
+-- Forum: [INDEX] (https://mklab.gr/forumdisplay.php?fid=1)
+--- Forum: MATHEMATICS (https://mklab.gr/forumdisplay.php?fid=3)
+---- Forum: ARTICLES (https://mklab.gr/forumdisplay.php?fid=13)
+----- Forum: AI AND TECHNOLOGY (https://mklab.gr/forumdisplay.php?fid=158)
+----- Thread: Formalizing 100 Theorems (/showthread.php?tid=1851)
Formalizing 100 Theorems - mklabgr - 09-04-2026
The “Formalizing 100 Theorems” project, maintained by mathematician and computer scientist Freek Wiedijk, tracks the progress of formalizing a well-known “Top 100” list of important mathematical theorems using computer proof assistants. A formalized theorem is not merely written as an ordinary mathematical proof: every definition, logical step, and inference is encoded in a rigorous formal language so that a proof-checking system can verify it mechanically. The list ranges from classical results such as the irrationality of $\sqrt{2}$, the Pythagorean theorem, and the infinitude of primes to much deeper results such as Gödel’s incompleteness theorem, the Prime Number Theorem, quadratic reciprocity, and the Fundamental Theorem of Algebra. According to the current project page, 99% of the 100 theorems have now been formalized in at least one system.
The project also serves as an informal benchmark for comparing major interactive theorem provers and formal mathematics libraries. It records which systems have formalizations for each theorem, including HOL Light (95 theorems), Isabelle (92), Lean (82), Rocq/Coq (80), Metamath (74), Mizar (71), ACL2 (48), and ProofPower (43), among others. The aim is not to catalogue every existing proof but to show how broadly different proof assistants can handle substantial mathematics. In this sense, the project documents the remarkable growth of formal mathematics: results that traditionally existed only as human-readable arguments are increasingly being converted into completely machine-verifiable proofs, laying important foundations for computer-assisted mathematics and, increasingly, AI-assisted theorem proving. [/url]
[url=https://www.cs.ru.nl/~freek/100/]PROJECT