Weekly
News about Lean, the theorem prover and programming language.
Lean releases, the compiler, tactics, Lake, Verso, libraries, kernels, and checkers. 142 items, newest first.
Wojciech Nawrocki merged a Yjs-based collaboration server that syncs changes between clients, plus collaborative editing support in the vscode-workbench extension. A separate change makes it impossible for openvscode-server instances to make requests against other instances.
Checked against: lean-workbench#14lean-workbench#12lean-workbench#18lean-workbench#17
A merged Lean pull request by Sebastian Graf gives the Sym-based mvcgen' feature parity with mvcgen, except +jp (join-point handling), at a cost of about 10% vcgen slowdown for cleaner user-visible VCs. A separate change adds whileM, which makes repeat/while loops verifiable with mvcgen.
Checked against: lean4#13578lean4#13209lean4#13672lean4#13582
One merged Lean 4 pull request fixes a Sym.simp panic triggered when match reduction exposed kernel projection terms, for example in a do block with a for loop over tuple state. Another removes an incorrect assertion that failed on have-expressions whose binder type depends on an earlier binder.
Checked against: lean4#13635lean4#13611lean4#13612
A pull request by Wojciech Nawrocki, merged on 2026-05-05, adds a VSCode extension to integrate it with the workbench in the leanprover/lean-workbench repository. The change also adds a launch target and server endpoint to debug the extension.
Checked against: lean-workbench#9
Mac Malone's merged pull request lets a Lean-written initializer add a constant to the Python module, adds Lean-side argument validation, and adds a Lean-to-Python-to-Lean test. A second merged change splits the global Python state (g_py_main) from the per-use GIL context (py_context).
The merged pull requests fix grind's AC invariants, a congruence-table panic, cast internalization order and missing proof hints. A new ringMaxDegree option (default 1024) bounds polynomial degree in the ring solver, and derived tactics such as lia, linarith and ring now fail quickly on out-of-scope problems.
Checked against: lean4#13593lean4#13585lean4#13590lean4#13624lean4#13625lean4#13623lean4#13614lean4#13622
nanobruijn, an experimental Lean 4 type checker in Rust forked from nanoda_lib, keeps expressions as pure de Bruijn indices with shift-homomorphic caching, and type-checks all of Mathlib (670k declarations) with 0 errors and 0 timeouts. The code changes were written by Claude (Anthropic), directed by Joachim Breitner.
Checked against: nomeata/nanobruijn
A merged pull request by David Thrane Christiansen adds a full-page search to Verso, accessed by pressing enter in the search field. The page shows more results, provides more context, and has more filtering features.
Checked against: verso#847
The new grind.ematch.diagnostics option tracks how E-matching theorem instances depend on each other, and a ringMaxDegree option (default 1024) bounds polynomial degree in the grind ring solver. Other merged pull requests fix beta reduction to respect the generation threshold, fix a kernel error for Nat casts to non-Int types, and extend the homomorphism demo.
Checked against: lean4#13558lean4#13585lean4#13560lean4#13453lean4#13532lean4#13520
Wojciech Różowski upstreamed the dupNamespace and unnecessarySeqFocus linters from Batteries to core Lean as "clippy" linters, which are disabled by default and run with lake lint --clippy. lake lint --builtin-lint now also supports text linters, and a new script reports deprecated modules, options and syntax usage.
Checked against: lean4#13513lean4#13538lean4#13540lean4#13586
A pull request by Wojciech Różowski, merged on 2026-04-22, adds builtin environment linting support to Lake, accessible via lake lint flags such as --builtin-lint and --clippy. It also introduces two builtin linters upstreamed from Mathlib (defLemma and checkUnivs) and a builtinLint package configuration option.
Checked against: lean4#13431
The pull requests fix a bug where satellite solvers (lia, ring, linarith) in sym => interactive mode threw an internal error, prune goals assigned by isDefEq, stop Sym.intros from assigning a metavariable when it introduces no binders, and restore eta-reduction of Sym.simp patterns containing loose pattern variables.
Checked against: lean4#13472lean4#13474lean4#13451lean4#13448lean4#13452
A merged pull request by Marc Huisinga adds three commands (Find, Copy, and Insert Unicode Symbol) that search symbols by abbreviation or by symbol, making it easier to insert Unicode into non-editor dialogs. Copy and Insert are bound to Ctrl+Alt+\ depending on whether a text editor is focused.
Checked against: vscode-lean4#762
Nerodia is a library for Lean/Python FFI inspired by PyO3 that uses Lake, Lean's build system, and generates type stubs for editors. It has a very limited API and is released primarily as a proof-of-concept and to obtain feedback on its design and build process.
Checked against: leanprover/nerodia
A HackMD note proposes to "separate the cheap default from the expensive exploration": a default grind mode that is cheap, fast and fails quickly, plus explicit named tactics such as nonlinear_ineqs and fin_cases that users, grind?, or AI invoke to produce replayable scripts.
Checked against: hackmd.io
The leanprover/verso-blueprint package, for writing Blueprint documents in Verso, now publishes Verso ports of the FLT and Sphere Packing blueprints, while Noperthedron and Carleson sit outside the catalog on the retired 4.34 line. Emilio Jesús Gallego Arias's porting harness has a human use Codex CLI to carry out the porting work.
Checked against: leanprover/verso-blueprintejgallego.github.ioejgallego/leanblueprint-to-verso
Leo de Moura merged pull requests adding Sym.Arith infrastructure for arithmetic normalization, fixing the sym canonicalizer, and adding a backward.isDefEq.respectTransparency.types option. An opt-in linter also warns about rfl simp theorems that only hold at higher transparency, part of a broader effort to ensure isDefEq respects transparency levels.
Checked against: lean4#13289lean4#13317lean4#13280lean4#13271lean4#13272lean4#13273lean4#13281
A merged pull request by Kim Morrison makes the transparency hierarchy none < reducible < instances < implicit < default < all, so @[implicit_reducible] annotations no longer have the side effects @[instance_reducible] has. A separate open pull request by Leo de Moura enables the backward.isDefEq.respectTransparency.types option by default.
Checked against: lean4#13637lean4#13283
Leo de Moura opened a pull request enabling the backward.isDefEq.respectTransparency.types option by default, so the definitional equality checker respects the current transparency setting when matching metavariable types. The change prevents unintended unfolding of definitions and requires adding @[implicit_reducible] and @[expose] attributes to many library definitions.
Checked against: lean4#13283
The bundle tool creates self-contained Lean 4 bundles for teaching: students download a zip, unpack it, double-click "Start_Lean", and get a working editor with no installation, no network access, and no command line needed. Each bundle ships VSCodium with the lean4 extension and only the oleans the project needs.
Checked against: leanprover-community/bundle
The release changes reducibility handling: isDefEq no longer bumps transparency when comparing implicit arguments, and a new @[implicit_reducible] attribute and a backward-compatibility option ease migration. It also adds grind support for higher-order Miller patterns, mvcgen support for specifications in the local context, and faster startup.
Checked against: v4.29.0 release noteslean4 v4.29.0
A merged pull request by Henrik Böving ports the C emission pass from IR to LCNF. The PR describes this as the last step of the IR/LCNF conversion, enabling end-to-end code generation through the new compilation infrastructure.
Checked against: lean4#12781
In Lean, structure field defaults can now depend on fields that come before and after them, and dotted function notation supports explicit mode (@.f) and explicit universes (.f.{u,v}). Field notation such as e.f.{u,v} now also accepts explicit universe levels, fixing a bug where levels were attributed to the wrong expression.
Checked against: lean4#12841lean4#13245lean4#13262
The CSLib contributing guide covers two pillars: formalising computer science as reusable infrastructure, and code reasoning about mainstream programming languages via Boole, intermediate representations, and VC generation. Contributors who use AI must explain which tools they used in the PR description, following the Mathlib policy.
Checked against: leanprover/cslib