4 ms·
Comparing these different approaches is not trivial, of course. One view is to look at "Formalizing 100 Theorems" by Freek Wiedijk, which lists 100 mathematica
by dwheeler 7y ago
Comparing these different approaches is not trivial, of course.
One view is to look at "Formalizing 100 Theorems" by Freek Wiedijk, which lists 100 mathematical theorems and the various systems that have formalized a nontrivial number of them. It's basically a "challenge list" for these kinds of systems:
http://www.cs.ru.nl/%7Efreek/100/ http://www.cs.ru.nl/%7Efreek/100/
This list is discussed in "Formal Proof - Getting Started" (Freek Wiedijk, Notices of the AMS, Volume 55, Number 11, December 2008).
That list is absolutely not the only way to compare different tools. Still, it gives you a sense of how far along each one has come in actually making proofs. Here's the current status:
HOL Light 86
Isabelle 83
Metamath 71
Coq 69
Mizar 69
ProofPower 43
Lean 29
nqthm/ACL2 18
PVS 16
NuPRL/MetaPRL 8
As you can see, the top ones today are HOL Light, Isabelle, Metamath, Coq, and Mizar. Lean has far fewer, but to be fair it's also much newer.