Will Lean have proved the most theorems on Freek's list by beginning of 2024?
21
Ṁ300Ṁ1.6kresolved Jan 1
Resolved
NO1H
6H
1D
1W
1M
ALL
This resolves YES if, on December 31st 2023, Lean (or Lean 4) is at the top of the list of theorem provers maintained on Freek's website. This site will be used as the resolution source, but if the site can't be accessed for some reason at that time, I'll use the most recent version on the internet archive.
Sep 27, 2:14pm: If Lean is tied for 1st, I will resolve to 50%.
This question is managed and resolved by Manifold.
Market context
Get 
1,000 to start trading!
1,000🏅 Top traders
| # | Trader | Total profit |
|---|---|---|
| 1 | Ṁ150 | |
| 2 | Ṁ60 | |
| 3 | Ṁ36 | |
| 4 | Ṁ16 | |
| 5 | Ṁ13 |
Sort by:
People are also trading
Related questions
Which theorems will be officially formally proven in Lean by the end of 2028?
What tactic will prove the most mathlib lemmas at the end of 2026?
Which theorem prover will have proved the most theorems on Freek's list by end of 2028?
Will Fermat's last theorem proof be completely formalized in Lean in 2026?
10% chance
Will Terence Tao write a paper with Lean code in it during the 2026 calendar year?
70% chance
Will fermats last theorem be formalized in lean down to the axiom in 5 years.
60% chance
Will Kevin Buzzard successfully fulfill his grant specs of formalizing Fermat's Last Theorem in Lean within 5 years?
64% chance
Will Lean mathlib contain more than 10 million lines of code by 2030?
67% chance
ZK tool for demonstrating one has proved math theorem (in Lean) created by EOY2026?
26% chance
Status of the Wentworth-Lorell conjecture in 2026