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.
A merged Lean pull request lets custom elements in Verso docstrings define their own Markdown rendering, which is used for LSP hovers and for legacy clients that don't directly support Verso. Example uses include including one docstring in another and showing all currently-available instances of a class.
Checked against: lean4#14115
Sebastian Graf merged pull requests renaming the experimental Sym-based mvcgen' tactic to vcgen, speeding up its matching, and adding a frames clause. A new @[frameproc] attribute lets a program type register how it frames a resource, so cost budgets, separation-logic footprints, and trace invariants frame through the same mechanism.
Checked against: lean4#14195lean4#14146lean4#14167lean4#14134
A merged pull request lets about 389 elab tests that use import Lean reuse one pre-built snapshot, cutting CPU time by 26.0% (2222 s to 1645 s), with CI test wall-clock speedups of about 10-40% depending on platform. Related pull requests speed up .olean and snapshot serialization, one cutting snapshot save time by about 28%.
Checked against: lean4#14077lean4#14109lean4#14122
Julia Markus Himmel added Float.Model, a pure Lean implementation of 64-bit floating-point numbers, and made Float a wrapper around it, so float operations are no longer opaque to the kernel while compiled code still uses native operations. Users can now prove 0.1 + 0.2 != 0.3 with rfl.
Checked against: juliahimmel.delean4#14079lean4#14091lean4#14110
Sebastian Graf merged a port of the experimental mvcgen' tactic to the new Std.Internal.Do meta theory, where loop invariants no longer restate the exceptional postcondition. A follow-up extracts a WP type class from WPMonad, enabling verification of deeply embedded languages, tested on an IMP language whose WP instance has no accompanying WPMonad.
Checked against: lean4#14080lean4#14015
Paul Reichert's merged pull request makes Lean compare metavariable types at implicit transparency instead of default, building on Kim Morrison's split of transparency into implicit and instances levels (merged on 2026-06-19). Some lemmas may stop applying in simp or grind; set_option backward.isDefEq.respectTransparency.types false restores the old behavior.
Checked against: lean4#13895lean4#13637
A merged pull request by Henrik Böving changes the m_imp field of lean_task to an atomic. get_task_state_core read m_imp to check whether a task had finished before taking the mutex, so that memory access was undefined behavior (UB).
Checked against: lean4#14108
A pull request by Mac Malone, merged into leanprover/lean4, has Lake deduplicate artifacts by their hash when uploading or downloading to the cache (for example in lake cache put or lake cache get). The change fixes possible errors when curl was asked to transfer to the same file or URL multiple times.
Checked against: lean4#14060
Lean 4.31.0 lands 305 changes, including while let loops in do blocks, a built-in Lake linting framework, stricter transparency handling in definitional-equality checking, and the experimental mvcgen' tactic, which can outperform mvcgen by over 100x on some synthetic benchmarks. The bundled toolchain moves from LLVM 19 to LLVM 22.
Checked against: v4.31.0 release noteslean4 v4.31.0
A merged Lean 4 pull request by Wojciech Różowski makes the cbv tactic available inside grind's interactive sym => mode. The tactic reduces the goal using call-by-value evaluation, supports at locations for hypotheses, and closes equation goals via refl when reduction finishes the proof.
Checked against: lean4#13971
Pull request leanprover/lean4#12030, "feat: link OpenSSL" by Sofia Rodrigues, was merged on 2026-06-05. The pull request was opened on 2026-01-16 and describes its change as linking OpenSSL.
Checked against: lean4#12030
The leanprover/hex repository installs the released hex libraries at a single pinned set, including HexLLL for LLL lattice reduction and HexBerlekampZassenhaus for integer polynomial factorization. Each computational library is Mathlib-free, with Mathlib correspondence proofs in a separate theory library.
Checked against: kim-em/hex
A merged pull request by Kim Morrison separates the levels so that @[implicit_reducible] annotations no longer have the side effects @[instance_reducible] has, such as allowing type class search to see through marked declarations. The hierarchy is now none < reducible < instances < implicit < default < all, and a new with_implicit tactic is added.
Checked against: lean4#13637
In a series of merged pull requests, Leo de Moura built infrastructure for a dsimp in SymM, functions for simplifying binders, reusable reduction DSimprocs (beta, zeta, zetaAll, dsimpProj, dsimpMatch), and syntax for declaring dsimp variants. The last pull request implements the dsimp tactic for interactive sym => mode.
Checked against: lean4#13857lean4#13823lean4#13824lean4#13825lean4#13854
The merged pull request adds impossible by t, which uses the tactic t to prove that the current goal is impossible, closing the original goal as if sorry were used. try? gains an impossible branch that runs impossible by decide, impossible by simp, and impossible by grind in parallel.
Checked against: lean4#13771
A merged pull request adds Lean.CompactedRegion.save and read, which save or load one module at a time with explicit sharing, generalizing the batch saveModuleDataParts API. Separate pull requests by Sebastian Ullrich make Lean's CI build everything with Lake and fold the Linux Lake job into the Linux release job.
Checked against: lean4#13185lean4#13721lean4#13759
A merged Lean pull request by Kyle Miller adds a tactic configuration system that supports custom configuration syntaxes, and on a simple benchmark configuration evaluation takes 6.2% of the time it used to. A separate pull request by Kyle Miller makes InfoView hovers include information about specific metavariables.
Checked against: lean4#13651lean4#13446
The leanprover/lean-workbench repository aims to provide familiar (VS Code with the Lean 4 extension) and novel interfaces to Lean online, giving each user an isolated Code Server instance inside a bubblewrap sandbox. The README warns the project is in progress and experimental, with a security audit forthcoming.
Checked against: leanprover/lean-workbench
Sebastian Ullrich's merged Lean pull request adds the Lake package option requiresModuleSystem: Lake then warns whenever a non-module-system file (one without a module header) imports a module of the package. A separate fix repairs code generation that broke with structures using private fields and types inaccessible in the current scope.
Checked against: lean4#13646lean4#13679
A demo chapter on x80.org previews foreign Rust references backed by a live language-server lookup: resolved references render a compact Rust source link and a grouped Rust code panel fetched from the location returned by rust-analyzer. A reference the language server cannot find is reported as unresolved, without a code panel.
Checked against: x80.org
The sos tactic is a sum-of-squares decision procedure for nonlinear real arithmetic, closely following John Harrison's HOL Light implementation. It calls the CSDP semidefinite programming library and rebuilds a fully certified result in Lean. Kim Morrison calls it a prototype and notes that frontier models have become very good at Lean metaprogramming.
Checked against: kim-em.github.ioLinkedIn post
In merged Lean pull requests by Leo de Moura, grind diagnostics now show local hypotheses used as E-matching theorems with their user-facing names and instantiation counters. A new grind option, genLocal, controls the maximum term generation for local theorems (for example, hypotheses) and defaults to 8, the same value as gen.
Checked against: lean4#13699lean4#13698
Compiled Lake configurations such as lakefile.olean now live in the workspace's .lake/config, removing a source of contention between workspaces sharing a dependency. Lake also now includes IR for a meta import's transitive imports, fixing "missing data file" errors with the artifact cache, and all Lake tests are re-enabled by default.
Checked against: lean4#13683lean4#13600lean4#13692
The pull request adds mvcgen', reimplemented from the ground up on the new SymM-based framework for efficient symbolic evaluation. It will soon replace mvcgen and can outperform it by a factor of more than 100 on some synthetic benchmarks. Join point sharing and introduction of local specs are not yet supported.
Checked against: lean4#13644