MANIFOLD
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
10
Ṁ450Ṁ3.3k
resolved Jan 1
100%98%
Isabelle
0.3%
Lean
0.4%
HOL Light
0.3%
Coq
0.2%
PVS
0.2%
Mizar
0.2%
Metamath
0.2%
nqthm/ACL2
0.2%
NuPRL/MetaPRL
0.2%
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.

Market context
Get
Ṁ1,000
to start trading!

🏅 Top traders

#TraderTotal profit
1Ṁ200
2Ṁ98
3Ṁ62
4Ṁ59
5Ṁ26
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.TermsPrivacy