The Lean development team is proud to announce the first milestone release of Lean 4. This release is aimed at experimentation with the new features of Lean 4, eventually leading to a full release of 4.0.0 ready for general use.

This release is the result of almost three years of work since the release of Lean 3.4.0, reworking, extending, and improving almost all aspects of Lean. More information about Lean 4 can be found in the official documentation as well as in the introductory talk "An overview of Lean 4" at Lean Together 2021.

Leonardo de Moura & Sebastian Ullrich

Acknowledgements

Daniel Selsam - type class resolution, feedback, design discussions Marc Huisinga and Wojciech Nawrocki - Lean Server Joe Hendrix, Andrew Kent, Rob Dockins, Simon Winwood (Galois Inc) - early adopters, suggestions, feedback Daan Leijen, Simon Peyton Jones, Nikhil Swamy, Sebastian Graf, Max Wagner - design discussions, feedback, suggestions