Karl Palmskog (Jun 20 2020 at 18:11): Karl Palmskog (Jun 20 2020 at 18:11):https://twitter.com/XenaProject/status/1273631847675813888
Will be interesting to see how the "99% automatic [porting of Mathlib]" will work out.
RUMOURS: (1) Lean 4 will be released "by the end of the summer"; (2) porting mathlib to Lean 4 will be "99% automatic". Source: reports from Zulip on Q&A after the Lean talk by the developers at PLDI2020. *Amazing* news! Slides http://leanprover.github.io/talks/LeanPLDI.pdf . #leanprover
- The Xena Project (@XenaProject) Cody Roux (Jun 20 2020 at 20:01):There was some debate about this point in the stream. I think attaching hard numbers like this is a bit unrealistic.
Karl Palmskog (Jun 20 2020 at 20:09):for precision, there is discussion in this Lean Zulip topic
Kevin Buzzard (Jun 21 2020 at 12:44):The source was some throw-away comments made after Leo's talk. There are certainly people in the Lean community who are skeptical about any kind of claim of this nature.
Last updated: Sep 28 2023 at 11:01 UTC