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)
There was some debate about this point in the stream. I think attaching hard numbers like this is a bit unrealistic.
for precision, there is discussion in this Lean Zulip topic
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: Jun 10 2023 at 06:31 UTC