Which theorem prover will have proved the most theorems on Freek's list by end of 2028? | Manifold

Which theorem prover will have proved the most theorems on Freek's list by end of 2028?

5

Ṁ175Ṁ175

2029

77%

Lean

10%

Isabelle

3%

HOL Light

3%

Coq

3%

Mizar

3%

Metamath

3%

Other

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.

The Lean Theorem Prover

Get

1,000

to start trading!

People are also trading

Which Erdos Problems will be solved before October 2026?

Which theorems will be officially formally proven in Lean by the end of 2028?

Will the alleged proof of P!=NP by Ke Xu and Guangyan Zhou be recognized as valid by 2050?

What tactic will prove the most mathlib lemmas at the end of 2026?

Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?

Will any of Levent Alpöge’s mathematical results with Claude be proven flawed by the end of the year?

By when will a competition platform like Codeforces but for mathematics (theorem proving) appear?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will AI be better every human at proving Math theorems by the end of 2030?

Related questions

Which Erdos Problems will be solved before October 2026?

Which theorems will be officially formally proven in Lean by the end of 2028?

Will the alleged proof of P!=NP by Ke Xu and Guangyan Zhou be recognized as valid by 2050?

What tactic will prove the most mathlib lemmas at the end of 2026?

Will a proof of Fermat's Last Theorem simple enough for Fermat to have possessed be found by 2027?

Will any of Levent Alpöge’s mathematical results with Claude be proven flawed by the end of the year?

By when will a competition platform like Codeforces but for mathematics (theorem proving) appear?

ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?

Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?

Will AI be better every human at proving Math theorems by the end of 2030?