Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
9
36
Ṁ528Ṁ102
resolved Jun 10
Resolved
YES1D
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.
Get Ṁ1,000 play money
Related questions
🏅 Top traders
# | Name | Total profit |
---|---|---|
1 | Ṁ14 | |
2 | Ṁ9 | |
3 | Ṁ7 | |
4 | Ṁ7 | |
5 | Ṁ6 |
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.
Theorem 81 is currently under review https://github.com/leanprover-community/mathlib/pull/7274
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