Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Mini
7
Ṁ931
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 Ṁ1,000 play money
Sort by:

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.