Blog
Posts
-
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