Stream: Miscellaneous

Topic: Lean 4 release end of summer

view this post on Zulip Karl Palmskog (Jun 20 2020 at 18:11):

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 . #leanprover

- The Xena Project (@XenaProject)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 20 2020 at 20:09):

for precision, there is discussion in this Lean Zulip topic

view this post on Zulip 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: Aug 19 2022 at 21:02 UTC