Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
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!
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.