Blog
-
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.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 FRO Year 1 in Review
As we reflect on the first year of the Lean FRO, we're proud to share our progress, challenges, and the foundational steps we've taken to ensure Lean's continued success and impact across diverse fields, including mathematics, software verification, and AI.
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.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 -
Functional induction
Proving properties of recursive functions is usually easiest when the proof follows the structure of the function that is being verified – same case splitting, same recursion pattern. To avoid having to spell this out in every proof, the upcoming 4.8 release of Lean provides a functional induction principle for recursive functions. Used with the
Read moreinductiontactic, this takes care of the repetitive parts of the proof. -
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. -
Quasiquotation with Binders: A Lean Metaprogramming Example
In programming languages research we often explore a language feature by formally defining a tiny language that is just big enough to have the properties we want, but is still small enough to make a fully self-contained formalization feasible. These tiny languages are typically not useful for actual programming, but it is often possible to encode more expressive features in the smaller language. Thus, the formal results can in principle apply to larger languages. Small models are also valuable for exploring new implementation techniques.
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 -
Recursive definitions in Lean
Lean is a general purpose programming language. For example, the Lean compiler itself is written in Lean, and so is its language server, which provides those nice squiggly lines that you see when you edit a Lean file. As a Lean developer, you can rightfully expect to be able to write the kind of code you’d be writing in other programming languages.
Read more -
The Lean Project Blog
Welcome to the Lean project's blog! Here, the core Lean developers will be posting announcements, tutorials, and other information that we think will be interesting to people who are not regular participants in the Lean Zulip chat.
Read more