Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
9
36
102
resolved Jun 10
Resolved
YES
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

🏅 Top traders

#NameTotal profit
1Ṁ14
2Ṁ9
3Ṁ7
4Ṁ7
5Ṁ6
Sort by:
bought Ṁ30 of YES
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.
bought Ṁ1 of YES
Theorem 81 has been accepted
bought Ṁ1 of YES
Theorem 81 is currently under review https://github.com/leanprover-community/mathlib/pull/7274
bought Ṁ5 of NO
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
bought Ṁ20 of YES
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.
bought Ṁ15 of YES
Looks like they need 4 more, though the remaining ones look relatively difficult: https://leanprover-community.github.io/100-missing.html