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 highlyvisible improvements.
New HashMap
and HashSet
Types
Lean 4.11 features a brandnew implementation of hash tables, concretely usable as both dictionaries (Std.HashMap
) and sets (Std.HashSet
).
This new implementation has been designed from the ground up for both efficiency and correctness, and it features an extensible, carefullyengineered framework for specifying and proving properties of its API.
Additionally, the API is a result of a careful comparison with both Lean's other data structures and with the hash table APIs of other languages, including both pure functional languages and imperative languages.
Updated variable
Command
The variable
command has been made more predictable in Lean 4.11.
This command is used to provide signatures in a single place for parameters that multiple declarations have in common, which reduces both the mental overhead of reading repetitive code and the risk of subtle inconsistencies.
In previous versions of Lean, when a variable
has been declared, any declaration in the scope of the variable
command may freely mention the declared variables.
Each mentioned variable, along with the variables that it depends on and any instance implicits that mention any included variables, are added as formal parameters to the declaration.
In Lean 4.11, this rule has been modified for theorems, so that only mentions of variables in theorem statements result in added parameters.
After this command, the names α
, β
, f
, and g
are variables:
variable
{α : Type u} {β : Type v}
(f : α → β) (g : β → α)
This definition of listMap
references the variable f
:
def listMap (xs : List α) : List β :=
match xs with
 [] => []
 x :: xs => f x :: listMap xs
Thus, its signature is:
listMap {α : Type u} {β : Type v}
(f : α → β)
(xs : List α) : List β
The variable g
is not part of the signature because it is not mentioned in the definition of listMap
.
Applying this rule to theorems has a drawback: if a variable is used in the body of a proof, then it becomes an assumption of the theorem. This means that the content of a proof can, in principle, affect the theorem statement. While Lean would always accurately report on the theorem statement, and there is no risk of inconsistency due to this behavior, it could be confusing. As an example, in Lean 4.10, one could write:
variable (n : Nat)
and then, after some intervening code:
variable (n_eq_zero : n = 0)
A user who did not notice the assumption that n = 0
might then attempt the following proof:
theorem n_plus_k_eq_k : n + k = k := n : Nat n_eq_zero : n = 0 k : Nat
⊢ n + k = k
All goals completed! 🐙
The theorem's type is:
n_plus_k_eq_k (n : Nat) {k : Nat} :
n + k = k
However, a second attempt to prove the theorem might make use of the variable and succeed.
This use may not be easy to see.
In n_plus_k_eq_k'
, simp_all
uses n_eq_zero
behind the scenes:
theorem n_plus_k_eq_k' : n + k = k := n : Nat n_eq_zero : n = 0 k : Nat
⊢ n + k = k
All goals completed! 🐙
Even though its statement appears identical to n_plus_k_eq_k
, the type of n_plus_k_eq_k'
is:
n_plus_k_eq_k' (n : Nat) (n_eq_zero : n = 0) {k : Nat} :
n + k = k
In Lean 4.11, the variable rule's interaction with proofs has been refined so that variables mentioned in the body of a proof no longer cause them to be inserted as parameters.
Only variables mentioned in the theorem statement itself are included.
The interaction between variable
and ordinary definitions has not been changed.
It can sometimes be convenient, however, to unconditionally insert a parameter across a swathe of definitions and theorems.
The new include
command causes a variable or variables to be unconditionally included as assumptions in theorems, regardless of whether they are mentioned.
Given this code in Lean 4.11:
variable (n : Nat)
variable (n_eq_zero : n = 0)
theorem n_plus_k_eq_k : n + k = k := n : Nat k : Nat
⊢ n + k = k
All goals completed! 🐙
include n_eq_zero
theorem n_plus_k_eq_k' : n + k = k := n : Nat n_eq_zero : n = 0 k : Nat
⊢ n + k = k
All goals completed! 🐙
the theorems have the following signatures, even though neither proof mentions n_eq_zero
:
n_plus_k_eq_k (n : Nat) {k : Nat} :
n + k = k
n_plus_k_eq_k' (n : Nat) (n_eq_zero : n = 0) {k : Nat} :
n + k = k
The effects of include
can be reversed using the omit
command.
Both include
and omit
can be used with in
to limit their effects to a single theorem.
To help limit the risk of unintended assumptions, a new linter issues a warning when an include
command results in probablyspurious assumptions:
theorem add_comm {x y : Nat} : x + y = y + x := n : Nat n_eq_zero : n = 0 x : Nat y : Nat
⊢ x + y = y + x
All goals completed! 🐙
automatically included section variable(s) unused in theorem 'add_comm': n_eq_zero consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them: omit n_eq_zero in theorem ... note: this linter can be disabled with `set_option linter.unusedSectionVars false`
The updated rules for variable
inclusion makes large Lean libraries easier to maintain over time by reducing the number of unpredictable changes, without sacrificing the convenience of variable
.
To ease porting proofs to Lean 4.11, a new option deprecated.oldSectionVars
can be used to locally switch back to the old variable
behavior.
Structural Recursion
In Lean, all functions must either terminate with a return value for all possible inputs or be declared partial
or unsafe
.
Termination is justified to Lean's logical kernel by translating the function into primitive recursors, which keeps the trusted code base small by not requiring a trusted termination checker.
Broadly speaking, this translation can either use the recursor for one of the function's parameters (structural recursion) or the recursor for a proof that some measure of the inputs decreases down to a minimal value (wellfounded recursion).
Structural recursion is simpler, leading to smaller and betterbehaved proof terms, while wellfounded recursion is much more flexible.
Lean is capable of automatically choosing a strategy for many programs, but because the problem is fundamentally undecidable, some functions must be annotated with a termination_by
clause that explicitly specifies why the function terminates.
Declaring Structural Recursion
In prior versions of Lean, termination_by
was to provide a decreasing measure for use with wellfounded recursion.
While this is useful when Lean otherwise would not accept a recursive definition, it is also useful when Lean successfully finds a decreasing measure, because it can speed up rechecking the function and document to readers why the function terminates.
However, there has not previously been a way to specify that Lean should use structural recursion to check termination, and the absence of a termination_by
clause could indicate either structural recursion or automaticallydetermined wellfounded recursion.
Furthermore, the termination_by?
syntax that caused Lean to offer to insert the measure that was found for wellfounded recursion into the code had the additional effect of requiring that the function use wellfounded, rather than structural, recursion.
Lean 4.11 removes these limitations by introducing the termination_by structural
clause, which allows structural recursion to be explicitly indicated.
For example, in the following code, the recursive call in the function findList
is on an immediatelysmaller list, while the recursive call in the helper function findArray.loop
is on a larger natural number:
def findList (p : α → Prop) [DecidablePred p] :
List α → Option {x : α // p x}
 [] => none
 x :: xs =>
if ok : p x then some ⟨x, ok⟩
else findList p xs
termination_by structural x => x
def findArray (p : α → Prop ) [DecidablePred p]
(xs : Array α) :
Option {x : α // p x} :=
let rec loop i :=
if h : i < xs.size then
if ok : p xs[i] then some ⟨xs[i], ok⟩
else loop (i + 1)
else none
termination_by xs.size  i
loop 0
Lean's termination analysis is capable of finding both termination arguments automatically, but it may be desirable to annotate the program nonetheless.
The prototypical example of a function that cannot be written with only structural recursion is Ackermann's function:
def ack : Nat → Nat → Nat
 0, n => n + 1
 m + 1, 0 => ack m 1
 m + 1, n + 1 => ack m (ack (m + 1) n)
termination_by x1 x2 => (x1, x2)
However, this is only true in languages without firstclass functions. With higherorder functions, Ackermann's function can be made structurally recursive:
def ack' : Nat → Nat → Nat
 0, n => n + 1
 m + 1, n => (n + 1).repeat (ack' m) 1
termination_by structural m => m
Documenting this in the termination_by
clause makes the two definitions' purposes clear to readers of the code.
Additionally, termination_by?
no longer forces Lean to use wellfounded recursion, and it can suggest a termination_by structural
clause if appropriate.
Mutual Structural Recursion
Mutually recursive datatypes naturally give rise to mutually recursive functions. In prior versions of Lean, mutually recursive functions always used wellfounded recursion in the core language. In Lean 4.11, however, mutual structural recursion is available.
Beginning in Lean 4.11, structural recursion can be used for mutually recursive functions, potentially even over mutually recursive datatypes. This brings the advantages of structural recursion to more functions.
For example, given the mutuallyrecursive types Tree
and Forest
:
mutual
inductive Tree (α : Type u) : Type u where
 leaf
 branch : α → Forest α → Tree α
inductive Forest (α : Type u) : Type u where
 empty
 trees : Tree α → Forest α → Forest α
end
Lean 4.11 is able to use structural recursion to count their elements or map a function over them:
mutual
def Tree.count : Tree α → Nat
 .leaf => 0
 .branch _ xs => 1 + xs.count
termination_by structural t => t
def Forest.count : Forest α → Nat
 .empty => 0
 .trees t ts => t.count + ts.count
termination_by structural ts => ts
end
mutual
def Tree.map (f : α → β) : Tree α → Tree β
 .leaf => .leaf
 .branch x xs => .branch (f x) (xs.map f)
termination_by structural t => t
def Forest.map (f : α → β) : Forest α → Forest β
 .empty => .empty
 .trees t ts => .trees (t.map f) (ts.map f)
termination_by structural ts => ts
end
Structural mutual recursion is also supported over nonmutuallyrecursive data:
mutual
def isEven : Nat → Bool
 0 => true
 n + 1 => not (isOdd n)
termination_by structural n => n
def isOdd : Nat → Bool
 0 => false
 n + 1 => not (isEven n)
termination_by structural n => n
end
Recursion Through Lists and Arrays
Many datatypes contain lists or arrays of themselves.
When writing recursive functions over these types, it is very convenient to use Array.map
, List.map
, or other higherorder functions from the standard library.
However, this pattern of recursion does not directly apply the recursive function to a smaller argument, as the recursive occurrence of the function is not syntactically applied to any argument whatsoever!
The function does terminate, however, because every argument that will ever be passed to the function is indeed smaller, but this reasoning is beyond what Lean's automation can derive on its own.
Lean 4.11 incorporates a solution by Mario Carneiro, originally part of the communityrun library batteries
, in which a helper function “attaches” to each element a proof that it is, in fact, a member of the list or array.
This is sufficient to enable Lean's automation to construct a termination proof using wellfounded recursion.
These helpers are called List.attach
and Array.attach
:
List.attach (l : List α) : List {x : α // x ∈ l}
Array.attach (xs : Array α) : Array {x : α // x ∈ xs}
As an example, the table of contents of a book can be represented with the datatype ToC
:
inductive ToC where
 content (title : String) (subContent : Array ToC)
The elements of the array represent the chapters in a book, the sections in a chapter, and so forth, as in this cookbook:
def cookbook : ToC :=
.content "Pea and Lentil Recipes" #[
.content "Introduction" #[],
.content "Soups" #[
.content "PalouseStyle Brown Lentil Soup" #[],
.content "Split Pea Soup" #[],
.content "Creamy Red Lentils" #[]
],
.content "Sandwiches" #[
.content "Lentil Sloppy Joes" #[],
.content "Chickpea Patty" #[]
],
.content "Salads" #[
.content "Lentil and Rice Confetti Salad" #[],
.content "Le Puy Lentils with Mint and Cucumber" #[]
]
]
Converting a table of contents to a string can be done with a recursive function that adds section numbers:
def prefixLines (pref content : String) : String :=
"\n".intercalate ((content.splitOn "\n").map (pref ++ ·))
partial def ToC.asString (toc : ToC) : String :=
let ⟨title, subContent⟩ := toc
let under := subContent.mapIdx fun i toc' =>
prefixLines s!"{i.val + 1}." (" " ++ toc'.asString)
s!"{title}{under.foldl (· ++ "\n" ++ ·) ""}"
#eval IO.println < cookbook.asString
Pea and Lentil Recipes 1. Introduction 2. Soups 2.1. PalouseStyle Brown Lentil Soup 2.2. Split Pea Soup 2.3. Creamy Red Lentils 3. Sandwiches 3.1. Lentil Sloppy Joes 3.2. Chickpea Patty 4. Salads 4.1. Lentil and Rice Confetti Salad 4.2. Le Puy Lentils with Mint and Cucumber
The function must be partial because Lean is unable to automatically conclude that argument in the recursive call is smaller:
def ToC.asString (toc : ToC) : String :=
let ⟨title, subContent⟩ := toc
let under := subContent.mapIdx fun i toc' =>
prefixLines s!"{i.val + 1}." (" " ++ toc'.asString)
s!"{title}{under.foldl (· ++ "\n" ++ ·) ""}"
termination_by toc
failed to prove termination, possible solutions:  Use `have`expressions to prove the remaining goals  Use `termination_by` to specify a different wellfounded relation  Use `decreasing_by` to specify your own tactic for discharging this kind of goal title : String subContent : Array ToC toc' : ToC ⊢ sizeOf toc' < 1 + sizeOf title + sizeOf subContent
However, using Array.attach
to add a proof that toc'
is an element of subContent
provides sufficient information for Lean to conclude that it terminates:
def ToC.asString (toc : ToC) : String :=
let ⟨title, subContent⟩ := toc
let under := subContent.attach.mapIdx fun i ⟨toc', elem⟩ =>
prefixLines s!"{i.val + 1}." (" " ++ toc'.asString)
s!"{title}{under.foldl (· ++ "\n" ++ ·) ""}"
List.attach
and Array.attach
have no runtime overhead in compiled code.
The compiler erases proofs, and they are implemented with a special optimization that removes the traversal of the list.
UserDefined Options
Lean's options system allows users to configure various properties of Lean, such as the maximum recursion depth during tactic execution, whether to display tracing output, and how many columns to use when displaying output.
The set of options is extensible, so userdefined tactics and other extensions can provide a consistent interface through the set_option
command.
In prior versions of Lean, builtin options could additionally be configured by passing the D
flag to Lean on the command line or by setting the leanOptions
field in lakefile.toml
or lakefile.lean
.
In Lean 4.11, userdefined options can also be set this way.
By default, Lean validates option names from the command line, ensuring that they are defined.
This helps avoid typos.
To turn off this checking, prefix an option name with weak.
.
For example, if a user option for a custom tactic squish
is named theorem_squisher.attempts
, then
[[lean_lib]] name = "AmbitiousProof" leanOptions = { theorem_squisher.attempts = 40 }
will fail if theorem_squisher.attempts
has not yet been defined, while
[[lean_lib]] name = "AmbitiousProof" leanOptions = { weak.theorem_squisher.attempts = 40 }
will not.
Safer Evaluation
Unlike many programming languages, Lean does not have a separate readevalprint loop for interactive exploration.
Instead, Lean expressions can be evaluated directly in the program text, without having to switch contexts, using the #eval
command.
In previous versions of Lean, #eval
had a difficult interaction with another Lean feature: to provide better feedback on a whole program, Lean continues to check a file even after errors have been encountered.
In order for the rest of the file to make as much sense as possible, the errors are replaced with sorry
.
The Lean compiler will not compile code that contains errors.
However, in prior versions of Lean, #eval
would run erroneous code.
Because the sorry
can occur as a replacement for a proof of some important property, such as array access being inbounds or a function terminating, #eval
could cause the compiler to crash or loop.
In Lean 4.11, #eval
no longer runs code that contains sorry
.
In this example, there are two errors:
def arr := #[1, 2, 3]
#eval arr[3]
The first comes from the array lookup, which fails due to the index being out of bounds.
The second comes from #eval
:
cannot evaluate expression that depends on the `sorry` axiom. Use `#eval!` to evaluate nevertheless (which may cause lean to crash).
A new command #eval!
can be used to evaluate expressions that depend on sorry
.
Lake
Lake, the Lean build tool, now includes a basic GitHub Actions configuration when it generates a new project.
This configuration uses leanaction
to build, test, and lint the project.
leanaction
is developed and maintained by Austin Letson.
Standard Library
In addition to the brandnew Std.HashMap
and Std.HashSet
, Lean 4.11 includes a number of additions to the standard library, many of which originate in the batteries
community library.
In particular, many lemmas about lists, arrays, bitvectors, and bitwise operators are either new or have been upstreamed from batteries
in Lean 4.11.
Tactics
Extensionality Lemmas
Extensionality is the principle that two objects are equal if all possible observations that can be made on them have equal results.
For functions, this means that applying them to equal arguments results in equal values.
For structures, it means that all fields have equal values.
The ext
tactic selects an appropriate extensionality lemma from a table and applies it.
There is an attribute called @[ext]
with two uses:

Applied to extensionality lemmas, it registers them for use with the
ext
tactic. 
Applied to structure declarations, it generates and registers extensionality lemmas for the tactic.
In Lean 4.10, the attribute would also generate a bidirectional extensionality lemma for structures that strengthens "equal observations imply equal values" to "equal observations is logically equivalent to equal values", named ext_iff
.
In Lean 4.11, the attribute now arranges for lemmas to be generated ondemand, rather than doing it upfront.
When used to register a userwritten extensionality lemma, it also automates the construction of the corresponding ext_iff
lemma.
In both Lean itself and in Mathlib, this has made it possible to delete many manual proofs, and the resulting generated lemmas are more consistent with each other.
Additionally, in Lean 4.11 the @[ext]
attribute now supports use as local
or scoped
attribute, allowing more finegrained control over the lemmas.
Local attributes only have an effect in the current section or namespace declaration, while scoped attributes have an effect in the current namespace or any other context that open
s it.
Improved Error Messages
The decide
tactic, which can solve a proof goal using a decision procedure (expressed as a Decidable
instance), now features significantly improved error messages.
This tactic can fail for a number of distinct reasons:

The goal may contain free variables that prevent the decision procedure from running to completion.

The goal may in fact be false.

The decision procedure may have been defined noncomputationally, either using classical reasoning or tactics that don't generate executable code.
In Lean 4.7, decide
's error messages were made explicit about the reason for failure.
Lean 4.11 builds on that work, further improving the error message.
Starting in version 4.11, the error message includes information about which specific Decidable
instances were unfolded.
It recognizes a number of common reasons that an instance may not be computable and provides specific guidance on remedying the situation.
It can even pinpoint the specific instance that is at fault.
Breaking Changes
 Signatures and visibility of generated extensionality lemmas
In
ext
andext_iff
lemmas that are generated by the@[ext]
attribute, thex
andy
term arguments are now implicit. Additionally, these two lemmas are now protected, so opening their namespace will not make them visible without a prefix. Please refer to pull request #4543 for more details and context. Typo fix in option name
The name of
trace.profiler.useHearbeats
has been corrected totrace.profiler.useHeartbeats
. Structural recursion
A bug in the elaboration of structurallyrecursive functions allowed incorrect programs to be accepted, leading to their rejection later by the kernel due to function parameters not being in the order required for the elaboration to always work. However, it is possible that some mistakenlyaccepted programs could work nonetheless, because the translation rules are conservative. These programs are now rejected prior to reaching the kernel. Affected programs can be fixed by reordering their arguments as described in pull request #4672.

List.filterMapM
sequences monadic actions lefttoright Previously,
List.filterMapM
sequenced monadic actions from right to left, even though the result values were returned from left to right. This bug has been fixed, but code that relied on the prior behavior may need updating. The effect of the
variable
command on proofs oftheorem
s has been changed. Please see the dedicated section in this post for more details. The option
deprecated.oldSectionVars
can be used to temporarily switch back to the old behavior while updating code.