A question about LEAN

Stream: new members

[Darren Zhu]

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!

[Mario Carneiro]

• 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.

[Darren Zhu]

Thank you for the informative response!

[Patrick Massot]

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.

[Eric Wieser]

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.

[Darren Zhu]

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.

[Ruben Van de Velde]

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.)

[Kevin Buzzard]

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

[Julian Berman]

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.

[M.G.]

Hello Lean Community, I am fairly new to functional programming and would like to eventually learn Lean 4 as a language and for theorem proving purposes. Any advice on getting started for a complete beginner would be much appreciated. I have a few questions: 1) Should I learn Haskell first? 2) Would Haskell make me understand the basics of functional programming before starting on Lean 4?

[Kevin Buzzard]

What's your background?

[M.G.]

Kevin Buzzard said:

What's your background?

Computer Science, Statistical Learning Theory and Dynamic systems, Programming in C/C++ and Python.

[Kevin Buzzard]

then sure learn some Haskell, learning Haskell will definitely help you to understand the basics of functional programming and Lean is a functional language. There are far more resources out there for learning Haskell, but you can always spend some time looking at #tpil as well.