Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
7
82
450
2025
51%
Lean
39%
Isabelle
3%
HOL Light
3%
Coq
0.7%
PVS
1%
Mizar
1%
Metamath
0.7%
nqthm/ACL2
0.7%
NuPRL/MetaPRL
0.7%
ProofPower

Freek's list is here. If there's a tie, I will resolve with equal probability on all first place outcomes. Since there are sometimes delays, for the final number, I'll take the maximum of Freek's number and the number on any of the prover-specific pages linked by Freek at close time.

Get Ṁ200 play money
Sort by:
bought Ṁ10 of HOL Light YES

What do you do if there is a discrepancy between Freek's list and the list of one of the particular theorem provers (like this one: http://www.cse.unsw.edu.au/~kleing/top100/ ?)
I'm asking, because sometimes there is a multiple-month delay between the update on the specific theorem prover and Freek's list.

@FlorisvanDoorn Yes, the fact that the list sometimes takes time to get updated is an unfortunate arbitrary factor. I'll say that I'll take the maximum of Freek's number and any of the pages linked by Freek.

More related questions