Lean core, page 3

Lean releases, the compiler, tactics, Lake, Verso, libraries, kernels, and checkers. 142 items, newest first.

Mac Malone merges Lake remote cache fixes, tests, and a --package option

Lake now demotes cache failures during a build to trace-level messages, so builds run with --wfail or --iofail do not fail solely due to the cache, and lake cache get gains --package to fetch outputs for a specific workspace package. A new test mocks remote cache transfers with a mock Python HTTP server.

Checked against: lean4#14720 lean4#14724 lean4#14700

Lean core Aug 6

Lean speed site charts Mathlib build instructions across 25,000 commits

A graph on speed.lean-lang.org tracks mathlib4 build instructions over 25,000 commits, scaling older values to line up with newer ones across the move from the old speedcenter to radar and the switch to measuring only userspace instructions. Dashed lines mark the 90 toolchain bumps.

Checked against: speed.lean-lang.org

Lean core Jul 30

Sebastian Graf extends Lean's def contracts with requires and assert

Merged Lean pull requests by Sebastian Graf name the precondition clause of a def contract requires, pairing with ensures, let requires and invariant bind assertion arguments such as a state monad's state, and add an assert element to do notation that vcgen proves as a verification condition while doing nothing at runtime.

Checked against: lean4#14602 lean4#14589 lean4#14603 lean4#14614

Lean core Jul 25

bv_decide solves 2401 of 2540 benchmarks at SMT-COMP 2026

In the QF_Bitvec division of the SMT-COMP 2026 Single Query Track, bv_decide reached a correct score of 2401 with zero errors, ahead of cvc5 at 2375 and Z3-GEX at 2229. Bitwuzla-MachBV led the division with 2495.

Checked against: smt-comp.github.io

Lean core Jul 22

Patrick Hulin reports a kernel check gap allowing a proof of False

In leanprover/lean4#14484, Patrick Hulin reports that the kernel does not reject free variables in opaque declaration bodies, letting an adversarial metaprogram prove False with no axiom dependencies. The report, largely generated with AI, suggests applying the closure check used for definitions and theorems, and the issue is now closed.

Checked against: lean4#14484

Lean core Jul 18

Leo de Moura adds grind hom attributes to replace ToInt typeclasses

Leo de Moura merged pull requests adding a [grind homo] attribute, since renamed [grind hom] and [grind hom_pred], and migrated the standard library to them. The new approach will replace the ToInt typeclasses used in grind. Andres Erbsen has already successfully tried and prototyped it.

Checked against: lean4#14446 lean4#14468

Lean core Jul 17

Leo de Moura merges grind discharger support for Sym.simp and three fixes

Leo de Moura merged pull requests letting grind discharge hypotheses in conditional Sym.simp theorems, preventing grind timeouts on definitional equality checks for match-expression conditions, fixing a canonicalizer bug that made grind miss valid contradictions, and fixing grind dropping E-matching theorems from custom grind attributes.

Checked against: lean4#14425 lean4#14444 lean4#14439 lean4#14426

Lean core Jul 16

lean4web enables deflate compression for large websocket messages

A merged pull request by Jason (@jcreedcmu) enables per-message deflate compression for messages larger than 16MB in the websocket server behind lean4web, aiming to improve responsiveness of live.lean-lang.org. Full completions with Mathlib imported produce 20-40MB jsonrpc responses, which compress by a factor of 8-9x.

Checked against: lean4web#133

Lean core Jul 15

Lean v4.33.0 release candidate 1 is out

The Lean developers published release candidate 1 for Lean v4.33.0, which centers on a more responsive editor, automatic try? proof suggestions, improved lia and grind tactics, a Float type that is no longer opaque, and kernel soundness fixes. It also enables backward.isDefEq.respectTransparency.types by default, the change most likely to need attention when porting.

Checked against: v4.33.0 release notes lean4 v4.33.0-rc1

Lean core Jul 15

Paul Reichert fixes slowdown caused by Lean's stricter transparency default

A merged Lean pull request by Paul Reichert makes whnfMatcher use the WHNF cache at sub-default transparency. It fixes a performance regression from #13895, merged on 2026-07-06, which enabled backward.isDefEq.respectTransparency.types by default as a breaking change that gives users more control over what is unfolded.

Checked against: lean4#14323 lean4#13895

Lean core Jul 15

Leo de Moura merges three fixes to Lean's SymM and Sym.simp

Leo de Moura merged pull requests that improve support for offsets in the SymM matcher/unifier, fix Sym.simp failing to rewrite terms containing unassigned metavariables (a failure reported by Sebastian Graf), and stop preprocessType in SymM from performing zetaDelta by default.

Checked against: lean4#14404 lean4#14405 lean4#14401

Lean core Jul 14

Sebastian Graf adds frame inference and contract syntax to Lean's vcgen

Merged pull requests extend vcgen, described as a verification condition generator over the Std.Internal.Do metatheory, with automatic frame inference and with loop invariants and def contracts (require and ensures clauses) that vcgen discharges automatically. A showcase repository collects imperative Lean programs verified with one 'vcgen ... with finish'.

Checked against: lean4#14389 lean4#14195 sgraf812/vcgen-showcase leanprover/lean4

Lean core Jul 14

Leo de Moura adds liaSteps option and BitVec literal propagators to grind

A merged Lean pull request adds a liaSteps configuration option to grind, meant to quickly interrupt the search for hard linear integer arithmetic problems. A second merged pull request implements grind propagators that evaluate BitVec operations on literals.

Checked against: lean4#14392 lean4#14393

Lean core Jul 13

Lean v4.32.0 makes the new do elaborator the default

Lean v4.32.0 adds the do← marker for effect forwarding and cuts import Mathlib time by about 10% through a DiscrTree insertion fix. Lake's linting framework gains option-based control and module linters, and an experimental incremental-compilation mode lands behind CLI flags.

Checked against: v4.32.0 release notes lean4 v4.32.0

Lean core Jul 11

Sebastian Ullrich proposes prefix trees in oleans to speed up Lean imports

An open pull request by Sebastian Ullrich replaces hash maps built at import time with per-module prefix trees precomputed when oleans are written, cutting import Lean wall clock by 28% and mathlib's import phase by 21%, for about 6% larger stdlib oleans. A separate pull request by Sebastian Ullrich upgrading Lean to mimalloc 3 was merged.

Checked against: lean4#14362 lean4#7786

Lean core Jul 8

Wojciech Różowski adds two-phase stateful linters to Lean

A merged pull request lets linters persist and share state across command elaboration, with each stateful linter running an early phase and a late phase. Wojciech Różowski also changed the UnusedSimpArgs linter hint and split registerParametricAttribute as preparatory work for warning when @[deprecated] points at an already-deprecated declaration.

Checked against: lean4#14357 lean4#14344 lean4#14313

Lean core Jul 7

Kim Morrison releases first packages of Hex, a computational algebra library

The first Hex packages provide dense matrices, row reduction, Gram-Schmidt, and a verified implementation of the LLL lattice basis reduction algorithm, plus a version that delegates computation to the C library fplll while verifying a certificate. Specifications are written first, then AIs implement code and proofs, and a blog post runs the Coppersmith attack on RSA.

Checked against: kim-em.github.io kim-em/hex

Lean core Jul 7

Sebastian Ullrich merges editor whitespace fix and deterministic kernel recursion limit

Lean now reuses tactic results when only whitespace after a tactic changes, so progress is kept when preparing to type the next tactic. The kernel's deep recursion error is now bounded by the maxRecDepth option instead of the physical stack size, which is a breaking change that may require explicit maxRecDepth bumps.

Checked against: lean4#13956 lean4#11958

Lean core Jul 6

Leo de Moura adds rw and case tactics to Lean's sym mode

Merged pull requests by Leo de Moura implement the rw tactic and the case tactic (relevant for vcgen) in sym => mode, fix universe constraints and unresolved-instance reporting in SymM, add a hygienic parameter to intro-like functions, and speed up instance assignment when the goal type is ground.

Checked against: lean4#14287 lean4#14278 lean4#14277 lean4#14280 lean4#14279 lean4#14330 lean4#14314

Lean core Jul 3

Mac Malone merges new Lake APIs for dynamic libraries and linking

Lake adds Dynlib.runtimeOnlyDeps, for transitive dependencies that should not be linked but must be preloaded when precompiling, plus an API for retrieving the complete set of core dynamic libraries. A third change lets custom build targets link shared libraries or executables from a module without copying the code in LeanExe.recBuildExe.

Checked against: lean4#14254 lean4#14220 lean4#14219 lean4#14240

Lean core Jul 2

Lean 4 moves deferred docstring checks onto the linter framework

A merged pull request by David Thrane Christiansen adapts Lean's deferred docstring check mechanism to use the linter mechanism, replacing custom CI setup with an interface akin to environment linters and governed by the option linter.doc.deferred. In a breaking change, custom Verso docstring elements now use a two-constructor type.

Checked against: lean4#14206

Lean core Jul 1

Joachim Breitner adds automatic try? suggestions to Lean at common proof sites

A merged pull request by Joachim Breitner makes Lean suggest try? output for empty by blocks, unsolved goals, and sorry tactics, gated by three options that default to off. It replaces the tactic.tryOnEmptyBy option from an earlier pull request with a different implementation.

Checked against: lean4#13830

Lean core Jun 30

Wojciech Różowski opens Lean pull requests for stateful linters and unusedVariables hint

A now-closed pull request adds stateful linters: command linters that thread state from one command to the next, so a linter can accumulate information across a file. A merged pull request adds a hint to the unusedVariables linter, suggesting to rename the unreferenced name with an underscore.

Checked against: lean4#14225 lean4#14259

Lean core Jun 25

Henrik Böving adds cost metrics for grind's e-matching graph

A merged Lean pull request by Henrik Böving adds optional diagnostics, enabled via grind.ematch.diagnostics, that flag instances with many direct follow-up children and instances that participated in a large, transitive closure of follow-up instances. The metric is based on the cost heuristic of smt-scope, and thresholds are configurable.

Checked against: lean4#14118

More news