Will mathlib have formal proofs of 70 out of 100 theorems from Freek Wiedijk's list before July?
9
102Ṁ527
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
to start trading!

🏅 Top traders

#NameTotal profit
1Ṁ14
2Ṁ9
3Ṁ7
4Ṁ7
5Ṁ6
© Manifold Markets, Inc.TermsPrivacy