Week of Jul 16, 2026

Edition 22: 6 items published for Jul 9 to Jul 16, 2026.

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 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 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 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

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