Benefits of Lean 4

Stream: lean4

[Will Fourie]

Hi all, sorry if this is the wrong channel (was a bit split between this, general, and new members).

I am aware that Lean 4 is quite a big change compared to Lean 3, to the point that Lean 3 code is not compatible with Lean 4 (though there is some hope of an automated translation for at least some areas).

Given the scale of the work therefore required to move the Math Library, I wonder why the new version is worth this cost in time and effort? What does Lean 4 offer compared to Lean 3 that makes it worth it?

I have had a look on the main lean website but haven’t been able to find a specific “smoking gun” that jumped out as being a large upgrade, but this may just be due to me not being familiar enough with Lean to see the downsides of Lean 3.

[Kevin Buzzard]

For maths one benefit is a better typeclass system. It is true that there is mounting evidence that Lean 3 is "good enough" for mathematics, but basically we're greedy.

[Johan Commelin]

Also, compiled tactics will make automation faster.

[Marcus Rossel]

Also, from what I've heard, metaprogramming in Lean 3 had to be done by abusing the monad meant for tactics. In Lean 4 there's a coherent hierarchy of monads for different use cases.

[Will Fourie]

Great, thanks, I’ll give typeclasses a look in the new Theorem Proving in Lean 4 text.

@Marcus Rossel I am not sure what metaprogramming is or monads in this context, but I’ll give them a look, thanks

[Kevin Buzzard]

Also notation will be far more flexible, and mathematicians take notation seriously (the ideal is to have Lean code which looks as close as possible to mathematics written in unicode).

Metaprogramming/monads are to do with how tactics are written.

[Marcus Rossel]

Kevin Buzzard said:

Metaprogramming/monads are to do with how tactics are written.

They are also used to define notations/macros. So a better monad stack makes it easier to define (complex) math notation.

[Alex J. Best]

Some more points:

• In Lean 4 it is easier to create custom domain specific languages, which may be useful in mathematical projects.
• Lean 4 is maintained by the original developers currently, so there is more chance of bug reports receiving expert attention compared with the frozen lean 3.

[Will Fourie]

Ah, thank you for explaining. I guess that also helps answer the question of why Lean 3 code won’t work in Lean 4. If it did, then you’d presumably have to give up that feature due to having to carry tactics over

[Leonardo de Moura]

We (try to) address this question at the ICERM talk http://leanprover.github.io/talks/ICERM-2022.pdf (starting at slide 20).
The recording is available online here https://icerm.brown.edu/video_archive/?play=2906

[Scott Morrison]

A significant difference that hasn't really been mentioned here is that Lean 4 is a general purpose programming language (while Lean 3 wasn't quite). Having a functional programming language with an extremely expressive type system, that nevertheless compiles to efficient binaries is important for many potential use cases beyond just mathematics. (And the development of a "programming language ecosystem" around Lean 4 will be of immeasurable value even if you were only interested in the mathematics applications. This is part of the reason the library structure is developing differently already, with Std intermediate between the core language and mathlib4.)

[Arthur Paulino]

Another point: accessible FFI with C