Lean publishes fifth release candidate for v4.29.0
The Lean project published v4.29.0-rc5, the fifth release candidate for the v4.29.0 release of Lean, on GitHub on March 5, 2026.
Checked against: lean4 v4.29.0-rc5
Lean core, page 6
Lean releases, the compiler, tactics, Lake, Verso, libraries, kernels, and checkers. 142 items, newest first.
Nick Palladinos publishes SmtLibDsl, a type-safe SMT-LIB DSL for Lean 4
SmtLibDsl is a domain-specific language embedded in Lean 4 for writing SMT-LIB2 constraint programs, with backends including Z3, cvc5, Kissat, and CaDiCaL. Bitvector widths and enabled SMT theories are tracked at compile time, and Lean validates every decoded SAT model.
Checked against: palladin/SmtLibDsl
Lean v4.29.0-rc1 changes how isDefEq handles transparency on implicit arguments
Leo de Moura's lean#12179, merged on 2026-02-16, stops isDefEq from raising transparency to .default for implicit arguments, a behavior that caused scalability problems in Mathlib. Kim Morrison advises downstream projects not to move to v4.29.0-rc1 yet, and a later PR documents the design rationale behind the transparency hierarchy.
Checked against: leanprover.zulipchat.comlean4#12179lean4#12561
Lean v4.28.0 released with a symbolic simulation framework and grind extensions
Lean v4.28.0 adds a lightweight symbolic simulation framework that integrates with grind and enables verification condition generators, plus user-defined grind attributes, a solver mode for bv_decide, and a first_par combinator that runs tactics in parallel. The release landed 309 changes, including performance improvements in bv_decide.
Checked against: v4.28.0 release noteslean4 v4.28.0
Leo de Moura merges isDefEq transparency change into Lean core
The pull request stops isDefEq from raising transparency to .default when checking implicit arguments, which was creating scalability problems in Mathlib. The PR calls it a very disruptive change, reversible with set_option backward.isDefEq.respectTransparency false. Separately, Lean published the second release candidate for v4.29.0.
Checked against: lean4#12179lean4 v4.29.0-rc2
Leo de Moura adds higher-order Miller patterns to grind's e-matching
A merged Lean 4 pull request lets grind's e-matching engine keep lambda arguments as patterns when pattern variables are applied only to distinct lambda-bound variables. Previously such lambdas were ignored during matching, which limited theorems about combinators like List.foldl that take a function argument.
Checked against: lean4#12483
Leo de Moura adds a cache for isDefEqI results in Sym
A merged Lean 4 pull request by Leo de Moura caches isDefEqI results in Sym, since symbolic computation such as VC generators finds the same instances repeatedly. On the vcgen_deep_add_sub_cancel benchmark, speedups range from 30% to 37%, with goal_1000 dropping from 1663.1 ms to 1141.9 ms.
Checked against: lean4#12486
Leo de Moura merges two Lean core elaborator changes
Leo de Moura merged a pull request stopping isDefEq from raising transparency to .default for implicit arguments, which was creating scalability problems in Mathlib (old behavior: set_option backward.isDefEq.respectTransparency false). A second pull request fixes the type class resolution cache for classes with output parameters.
Checked against: lean4#12179lean4#12286
Leo de Moura tests Claude-assisted refactoring of Lean's grind and Sym modules
Leo de Moura opened leanprover/lean4#12448, a pull request that refactors the grind and Sym modules using Claude-assisted code transformations as an experiment in AI-aided code maintenance. The pull request is marked "do not merge".
Checked against: lean4#12448
Kim Morrison proposes making Mathlib's OrderDual a structure, prepared with Claude Code
A Mathlib pull request by Kim Morrison changes OrderDual from a type alias to a one-field structure, which prevents defeq abuse between a type and its order dual and requires explicit toDual/ofDual wrapping at type boundaries. The pull request notes it was prepared with Claude Code.
Checked against: mathlib4#35125
Leo de Moura's Lean change stops simp from simplifying instances by default
The pull request, merged on 2026-02-05, ensures simp does not "simplify" instances by default, since doing so creates non-standard instances that cause problems in Mathlib. The old behavior can be retrieved with simp +instances, and the backward compatibility flag for dsimp also deactivates the change.
Checked against: lean4#12244
Leo de Moura fixes Lean's type class resolution cache
A merged pull request to leanprover/lean4 makes the type class resolution cache properly cache results for type classes containing output parameters. Output parameter arguments, and universe levels that only appear in output parameter types, are erased from the cache key to avoid cache misses.
Checked against: lean4#12286
New leancall library lets Python code call Lean functions directly
A post titled "Calling Lean Functions As Python Functions" introduces leancall, a Python library for Lean-Python interop built on LeanInteract, which gives a Lean REPL as a Python library. Examples include a Lean controller balancing a gym cartpole environment and a Lean ray tracer displayed with Python plotting tools.
Checked against: philipzucker.com
Lean publishes leansqlite, SQLite bindings for Lean
The leanprover/leansqlite library bundles SQLite and adds interpolated strings that expand to prepared statements, plus iterators over query result rows. A Zulip user, pandaman, shared LeanToDo, an experiment in building a web application with Lean that uses leansqlite for its database and Verso for HTML templating.
Checked against: leanprover/leansqliteleanprover.zulipchat.com
Sebastian Ullrich's merged PR separates meta and non-meta code in Lean binaries
The change lets the module system, in cooperation with the linker, keep tactics used only in proofs out of the final native binary. A simple example using meta import Lean shrinks from 130MB to 1.7MB. As a breaking change, importModules (loadExts := true) must now be preceded by enableInitializersExecution.
Checked against: lean4#12016
Leo de Moura merges three Lean core changes to instance handling
Lean now identifies instance parameters by type using isClass? instead of binder syntax, dsimp no longer simplifies instances by default, and isDefEq no longer raises transparency to .default for implicit arguments, a change the PR calls very disruptive. Old behavior is available through backward.* options, and the PRs cite problems in Mathlib.
Checked against: lean4#12172lean4#12195lean4#12179
Willem Vanhulle builds a terminal user interface for Lean 4 users
Willem Vanhulle is putting together a TUI (a terminal-only user interface) for Lean4 users, built with Ratatui. The TUI has several display modes with different display styles for on-going mathematical proof development, and documentation is available.
Checked against: LinkedIn post
Lean repository adds SymM symbolic simulation benchmark from Lean@Google Hackathon
A new benchmark in the lean4 test suite, described as a synthetic benchmark from the Lean@Google Hackathon, compares a MetaM tactic solution with SymM solutions, including a "SymM Solution + reusing simplifier cache" variant, on generated command sequences of up to 700 iterations, also timing kernel checking.
Checked against: leanprover/lean4
Leo de Moura adds ground evaluation and conditional rewriting to Sym.simp
Three merged Lean 4 pull requests by Leo de Moura extend Sym.simp: a simplification procedure evaluating ground terms of builtin numeric types such as Nat, Int and BitVec n, support for conditional rewriting rules, and offset terms, essential for equational theorems of functions that pattern match on natural numbers.
Checked against: lean4#12031lean4#12033lean4#12053
Sebastian Ullrich proposes bundling Lean's Init library into one .olean file
A pull request by Sebastian Ullrich bundles all Init module files into a single file with cross-sharing, reducing cumulative size from 325MB to 264MB and openat calls for import Init on Linux from about 2000 to about 80. The pull request is still open.
Checked against: lean4#11965
Leo de Moura removes super-linear kernel overhead in lambda simplification
A merged Lean pull request by Leo de Moura improves the proof term produced by mkFunext, which Sym.simp uses when simplifying lambda expressions. For a 200-lambda benchmark, kernel checking time fell from 148.681 ms to 6.903 ms, and the approach will later come to Meta.simp.
Checked against: lean4#11932
Leo de Moura adds benchmarks showing SymM beating MetaM on intros/apply
A merged Lean 4 pull request by Leo de Moura adds performance comparison tests between the new SymM monad and the standard MetaM for intros/apply operations. Results show a 10-20x speedup, rising from 10.8x at size 1000 to 22.0x at size 6000.
Checked against: lean4#11838leanprover/lean4