Release Announcements
-
Lean 4.14.0
We're thrilled to announce Lean 4.14.0, which brings an array of improvements and new features to both the language and its tooling.
Read more -
Introducing the Lean Language Reference
The new Lean reference manual is officially released, just in time for your holiday projects!
The reference manual will be a comprehensive, concise, and accurate description of Lean. Even though it’s not yet totally comprehensive, it does contain descriptions of the tactic language, the most important parts of the term language, inductive datatypes and structures, and details about the elaboration process. Built using the documentation authoring DSL Verso, the reference manual includes tests that help us keep it up to date as Lean improves.
Read more -
Lean 4.11.0
We're delighted to announce that a new release of Lean, version 4.11.0, is now available. As usual, we've made a number of improvements to Lean's internals, and Lean 4.11 is more predictable, more responsive, and more reliable than prior versions. The improvements range from getting the details of hovers on parentheses just right to better debugging tools for proof automation developers to large performance increases to certain subsystems in Lean's internals. There is no way for this post to capture all of the hard work that's gone into the more than 250 separate commits that have been made to Lean's since the last release—please refer to the official release notes for a complete accounting, or read on for a selection of highly-visible improvements.
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. -
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.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.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.12.0
We are pleased to announce the release of Lean version 4.12.0! This release includes significant additions to tactics, performance, and Lake packages.
Please see the detailed release notes for the complete list of changes.
Read more -
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.10.0
We're happy to announce that Lean 4.10.0 has been released! As usual, this release includes a number of improvements to Lean's internals that improve performance, predictability, and proof automation. Lean's support for incrementally checking proofs has been improved, the language server is more robust, there were improvements to the
Read moresplit,simp, andrwtactics, and the details of the behavior ofdef,example, andtheoremhave been made more consistent with each other. For a complete accounting, please refer to the release notes; read on for some highlights! -
Lean 4.13.0
We're thrilled to announce Lean 4.13.0, which brings an array of improvements and new features to both the language and its tooling.
Read more