Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
9
102Ṁ527resolved Jun 10
Resolved
YES1H
6H
1D
1W
1M
ALL
Mathlib (https://leanprover-community.github.io/) is a library of mathematics formalized in the Lean proof assistant. Like other mathematical formalization efforts, mathlib tracks the number of theorems it has formalized from the "100 theorems list" (https://www.cs.ru.nl/~freek/100/), a list of 100 well-known theorems proposed by Freek Wiedijk.
This question resolves to "YES" if, before the market closing time, the mathlib 100 theorems tracking page at (https://leanprover-community.github.io/100.html) indicates that 70 or more theorems from the list are formalized in Lean. This site will be treated as the authoritative resolution source; theorems that are formalized but not admitted to the mathlib repository or not tracked on the page will not count.
May 9, 12:43am: As a helpful tip, see this page https://github.com/leanprover-community/mathlib/commits/master/docs/100.yaml for a list of edits to the file from which the resolution page is generated.
This question is managed and resolved by Manifold.
Get 
1,000 to start trading!
1,000🏅 Top traders
| # | Name | Total profit |
|---|---|---|
| 1 | Ṁ14 | |
| 2 | Ṁ9 | |
| 3 | Ṁ7 | |
| 4 | Ṁ7 | |
| 5 | Ṁ6 |
People are also trading
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
72% chance
Will we have a formalized proof of Fermat's last theorem by 2049-05-01?
91% chance
Which theorems will be formally proven in Lean by the end of 2028?
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance
When will we have a fully formalized proof of Fermat's Last Theorem?
Sort by:
Optional stopping theorem added https://github.com/leanprover-community/mathlib/commits/master/docs/100.yaml
https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2313690.20strong.20law.20of.20large.20numbers/near/280097477
I'm starting to get optimistic, seems like there are a few Freek problems in the pipeline.
2 have been added in the past month, and the last before that was in June, if I'm interpreting the history of this file correctly: https://github.com/leanprover-community/mathlib/commits/master/docs/100.yaml
I think there looks like there is still plenty of low hanging fruit in that list, so I'm more bullish. Though I don't know any lean, so maybe I'm underestimating the difficulty of this. But Green's theorem, Taylor's theorem, the Central Limit Theorem and Godel's Incompleteness theorem are so well understood that they should be easy to do in first order logic, and hence in some computable system.
Looks like they need 4 more, though the remaining ones look relatively difficult: https://leanprover-community.github.io/100-missing.html
People are also trading
Related questions
Which theorem prover will have proved the most theorems on Freek's list by end of 2025?
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will rw_search be able to replace >50% of mathlib proofs by 2025-11-26?
19% chance
What tactic will prove the most mathlib lemmas at the end of 2026?
Will we have a formalized proof of Fermat's last theorem by 2029-05-01?
72% chance
Will we have a formalized proof of Fermat's last theorem by 2049-05-01?
91% chance
Which theorems will be formally proven in Lean by the end of 2028?
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance
When will we have a fully formalized proof of Fermat's Last Theorem?