The columns, one at a time
The thirteen systems
These are the thirteen columns of the table, in his order: by how much of the hundred each has covered, 95 down to 8. He chose them by a rule he states plainly — the page "just shows formalizations in systems that have formalized a significant number of theorems, or that have formalized a theorem that none of the others have done".
Each entry below says what the system is, in words checked against that system's own site on 2026-08-12, and links two different places: the list ofthese theorems in that system, which is the link his page carries and is often kept by someone else entirely, and the system's own home. Where a claim could not be checked, the entry says less rather than more — one of the thirteen has no description at all, and says why.
HOL Light
95 of 100
Its own site calls it "a computer program written by John Harrison to help users prove interesting mathematical theorems completely formally in higher order logic". It is written in OCaml, and is the HOL-family system with, in its own words, "a much simpler logical core and little legacy code".
- 95 of its 95 entries link to a statement.
- It has 3 of the six theorems he marks as difficult.
- The only system to have done #43, The Isoperimetric Theorem, #50, The Number of Platonic Solids.
Isabelle
92 of 100
"A generic proof assistant", originally developed at Cambridge and TU München and now carrying contributions from institutions and individuals worldwide. Its Archive of Formal Proofs is a large body of machine-checked mathematics kept alongside the system itself.
- 92 of its 92 entries link to a statement.
- It has 3 of the six theorems he marks as difficult.
Lean
82 of 100
Describes itself as "an open-source programming language and proof assistant", developed by the Lean FRO. Much of the mathematics on this list is in mathlib, its community-built library, which its own site puts at over a million lines.
- 82 of its 82 entries link to a statement.
- It has 2 of the six theorems he marks as difficult.
Its hundred, on leanprover-community.github.io · Its own site
Rocq
80 of 100
"An interactive theorem prover, or proof assistant", dependently typed, and "formerly known as the Coq Proof Assistant" — the rename is recent enough that his page still links a list at a coq-era address. It is where all 37 of the constructive proofs on this list outside NuPRL live.
- 80 of its 80 entries link to a statement.
- 37 are marked as constructive proofs.
- It has 1 of the six theorems he marks as difficult.
- The only system to have done #32, The Four Color Problem.
Metamath
74 of 100
Unusual in kind: "a simple and flexible computer-processable language" rather than a tactic-driven prover. Proofs "include every step, no exceptions", and verifiers "do not make logical inferences; they just verify that the proof as stated is correct" — the main database is checked by five independently written verifiers in five languages. Created by Norman Megill, who is also credited on 13 of these formalizations.
- 74 of its 74 entries link to a statement.
- It has 1 of the six theorems he marks as difficult.
Mizar
71 of 100
The oldest of them: its site dates the project to a talk by Andrzej Trybulec in November 1973. Its language is "derived from the mathematical vernacular", meant to be "readable for mathematicians and, simultaneously, sufficiently rigorous to enable processing and verifying by computer software".
- 71 of its 71 entries link to a statement.
nqthm/ACL2
48 of 100
ACL2 is "A Computational Logic for Applicative Common Lisp", by Matt Kaufmann and J Strother Moore, and its own site places it in "the Boyer-Moore family of provers". His column merges it with nqthm, the earlier prover in that family: 44 of the 48 are credited to ACL2 and 4 to nqthm.
- 48 of its 48 entries link to a statement.
ProofPower
43 of 100
"A suite of tools supporting specification and proof in Higher Order Logic (HOL) and in the Z notation", begun in 1989 at International Computers Ltd to support "proofs of specification-to-model correspondence for high-assurance secure systems", and maintained by Lemma 1 since 1997. Rob Arthan is credited on all 43.
- 43 of its 43 entries link to a statement.
PVS
26 of 100
The Prototype Verification System, from SRI: "a mechanized environment for formal specification and verification" whose parts include a specification language, a type checker, an interactive prover and a model checker. Its own page credits NASA Langley's formal methods programme with much of the tooling and a library — which is why 15 of these formalizations are credited to "NASA library".
- None of its entries link to a statement on his page.
No list of its own: his page names these 26 entries without linking any of them. · Its own site
Imandra
20 of 100
The outlier here: a commercial automated reasoning engine from Imandra Inc. that comes at this from software verification rather than from mathematics — its own site is largely about translating source code into logic and checking properties of it. Its 100-theorems work is a repository rather than a library.
- 20 of its 20 entries link to a statement.
Megalodon
12 of 100
"An interactive theorem prover/proof checker based on higher-order Tarski-Grothendieck set theory", written in OCaml and the successor to Egal. Its own page situates it deliberately between AUTOMATH, Coq, Mizar and Metamath, and the HOL systems.
- 12 of its 12 entries link to a statement.
Naproche
10 of 100
The one whose input is meant to read like prose: "a natural proof assistant that models the usual reading and checking of mathematical proofs by mathematicians", using a controlled natural language embedded in LaTeX and handing the resulting obligations to automated provers.
- None of its entries link to a statement on his page.
NuPRL/MetaPRL
8 of 100
NuPRL/MetaPRL accounts for 8 of the hundred, all 8 of them marked as constructive proofs, and none of them linked on his page. No description here: its own site (nuprl.org) answered 403 over http and failed TLS over https when it was checked on 2026-08-12, in a browser as well as from the command line, so there was nothing to check a description against. Saying less is the honest option, and it is the rule this page follows.
- None of its entries link to a statement on his page.
- 8 are marked as constructive proofs.
No list of its own: his page names these 8 entries without linking any of them.
Counts are from a copy of his page as he last modified it on 2026-04-09. The descriptions are quoted or paraphrased from each system's own site, read on 2026-08-12; where his page's link for a system has rotted it has been repaired, and /about/ says which. Anything wrong here is mine, not theirs — corrections are welcome and easy to make, because every claim names where it came from.