Release Announcements
-
Lean 4.9.0
Lean 4.9.0 has been released! This release features a number of significant improvements to the user experience, better tools for diagnosing performance issues, and many more theorems in the standard library. Like every release, 4.9 also brings improvements to performance, predictability, and robustness to Lean's internals. There have been many more improvements to Lean since the release of 4.8.0 than there is space to discuss here—please refer to the release notes for a complete account.
Read more -
Lean 4.8.0
Lean 4.8.0 has been released!
Version 4.8.0 is a very big release, containing more than 370 separate improvements. There is no way for a single post to do justice to all of the hard work that has been put into this release. Many of the improvements have served to make Lean faster and more robust, but will be only visible because the whole system feels snappier and reliable. On the other hand, there were also a large number of directly visible enhancements—read on for some highlights!
Read more -
Lean 4.5.0
Lean version 4.5.0 has been released! This release contains a number of quality-of-life improvements.
Please see the detailed release notes for a complete list of changes.
Read more -
Lean 4.6.0
We're pleased to announce the release of Lean version 4.6.0! This is a big release, with significant improvements made to termination arguments, the simplifier, and the language server. On top of these headlines, there is the usual collection of improvements. The release notes contain more details.
Read more -
Lean 4.7.0
Lean 4.7.0 has been released! While this release includes the usual collection of quality-of-life improvements and bug fixes, the most noticable change is that a large part of
Read moreStd
, the external standard library, is included with Lean. Not only does this help with discoverability, it also enabled us to integrate these features more tightly into the rest of the language. In the next few releases, we'll continue to upstream data structures, tactics, proofs, and language features in order to make the out-of-box experience of using Lean as pleasant as possible.