Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
Resolved
YES
Jun 10
M$527 bet
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.

💬 Proven correct

Bolton Bailey made M$13!
BoltonBailey
Bolton Bailey bought M$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.
0
BoltonBailey
Bolton Bailey bought M$1 of YES
Theorem 81 has been accepted
0
BoltonBailey
Bolton Bailey bought M$1 of YES
0
horse
horse bought M$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
0
MrR
Mr R bought M$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.
0
Joris
Joris Kerkhoff bought M$15 of YES
Looks like they need 4 more, though the remaining ones look relatively difficult: https://leanprover-community.github.io/100-missing.html
0