Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Basic
7
Ṁ1338
2025
51%
Lean
38%
Isabelle
3%
HOL Light
3%
Coq
0.9%
PVS
1%
Mizar
1%
Metamath
0.9%
nqthm/ACL2
0.9%
NuPRL/MetaPRL
0.9%
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
and
S3.00
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.

© Manifold Markets, Inc.Terms + Mana-only TermsPrivacyRules