Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
8
450Ṁ1433Dec 31
39%
Lean
52%
Isabelle
2%
HOL Light
2%
Coq
0.8%
PVS
0.8%
Mizar
0.8%
Metamath
0.8%
nqthm/ACL2
0.8%
NuPRL/MetaPRL
0.8%
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.
This question is managed and resolved by Manifold.
Get 
1,000 to start trading!
1,000People are also trading
Related questions
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
2% chance
Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?
3% chance
Which theorems will be formally proven in Lean by the end of 2028?
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
70% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will we have a formalized proof of Fermat's last theorem by 2049-05-01?
91% chance
By when will a competition platform like Codeforces but for mathematics (theorem proving) appear?
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance