Zulip Chat Archive

Stream: new members

Topic: A question about LEAN


view this post on Zulip Darren Zhu (Dec 27 2020 at 03:45):

Hi! I'm new to LEAN and I have been looking into it (as well as other proof assistants) for a while now. The mathlib library is very impressive. I was wondering whether the eleven problems regarding LEAN addressed by Thomas Hales (https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/) have been either changed or resolved since the time of writing, particularly the problem regarding backward compatibility (of LEAN 4) and mathlib, and the "excessive parameterization" and taboo on "diamonds" that he addressed. Many thanks in advance!

view this post on Zulip Mario Carneiro (Dec 27 2020 at 04:06):

  • Backward compatibility - if anything it's become even less backwards compatible since that was written, although there are also possibilities for tools to ease the translation. It's all still up in the air.
  • Excessive parameterization - It depends on what you are doing. I think the presentation in the review is slightly overblown, but it's true that plenty of non-mathematical design decisions come in to the setup and use of the algebraic hierarchy.
  • Diamonds - These are not banned in mathlib, but there is a requirement that any diamonds commute up to defeq. It does necessitate the so-called "old structure command" (which isn't actually deprecated despite the name) because the new structure command bans diamonds outright.

view this post on Zulip Darren Zhu (Dec 27 2020 at 04:25):

Thank you for the informative response!

view this post on Zulip Patrick Massot (Dec 27 2020 at 09:48):

Darren, note that the backward compatibility thing is an issue only if you decide it is. We have good reasons to hope Lean 4 will be much better than Lean 3 in a way that would have been impossible if we were at a stage where backward compatibility is considered as important. And this point was extremely clear, nobody was taken by surprise.

view this post on Zulip Eric Wieser (Dec 27 2020 at 10:46):

Mario Carneiro said:

  • Diamonds - These are not banned in mathlib, but there is a requirement that any diamonds commute up to defeq

There are instance diamonds in mathlib (eg docs#add_comm_monoid.nat_semimodule and docs#linear_map.semimodule) which provably commute but not up to defeq.

view this post on Zulip Darren Zhu (Dec 27 2020 at 13:36):

Patrick, thanks for the information! It's great that Lean 4's development will be even better than Lean 3. When will Lean 4 be released approximately? And, when it does come out, will Mathlib be moved there and how will compatibility be managed? Thanks.

view this post on Zulip Ruben Van de Velde (Dec 27 2020 at 13:50):

My understanding is there's no timeline for lean 4 yet; mathlib will be moved there, but there's no clear plan of action yet. (Hopefully there will be a way to do it incrementally.)

view this post on Zulip Kevin Buzzard (Dec 27 2020 at 13:50):

Come to Lean Together 2021 and find out -- there will be discussions on this. Or just wait until after and then ask again :-)

view this post on Zulip Julian Berman (Dec 28 2020 at 14:34):

Looks like this got posted to HN this morning: https://news.ycombinator.com/item?id=25550240 in case anyone feels like mentioning any of the above in the comments there.


Last updated: May 14 2021 at 12:18 UTC