May 30th, 2026 · 3 commits
Lean 4 adds experimental closure serialization in `.olean` files, plus a small spec-db migration fix and docs cleanup.
Read the issue →
May 29th, 2026 · 9 commits
VC generation now tracks in-scope specs per subgoal, symbolic reducers gained new level/match fixes, and floating-point nondeterminism is blocked at compile time.
Read the issue →
May 28th, 2026 · 9 commits
+1
mvcgen' now handles typeclass method projections, lints were promoted into Lean.Linter, and parser/error polish landed too.
Read the issue →
May 27th, 2026 · 7 commits
Public lint imports, linter tagging, a mvcgen kernel fix, and a build-time ban on HWASAN/MTE make up the day’s notable work.
Read the issue →
May 26th, 2026 · 10 commits
New `dsimp` support in grind/sym, inline `mvcgen'` in `sym =>` blocks, better `whileM` foundations, and improved error notes.
Read the issue →
May 25th, 2026 · 5 commits
New `impossible` tactic combinator lands, `simpa using` gets stricter transparency, and `using!` is introduced as the opt-in escape hatch.
Read the issue →
May 24th, 2026 · 3 commits
Lean4 adds a new `SymM`-based `dsimp`, binder simplification, and reusable reduction simprocs for beta/zeta/projections.
Read the issue →
May 21st, 2026 · 8 commits
Notable fixes for inductive elaboration, proof-mode metadata, and Verso docstrings, plus `#where` scope reporting and a major app elaboration perf tweak.
Read the issue →
May 20th, 2026 · 7 commits
Lean4’s do-notation now handles indexed monads, while string comparison gets a faster C++ backend and path/string cleanups continue.
Read the issue →
May 19th, 2026 · 9 commits
Specialized `dec` lowering lands, config-eval bootstrapping is finished, and Lake/CI get reliability fixes.
Read the issue →
May 18th, 2026 · 10 commits
+1
Major tactic refactors, cache-key fixes, better premise selection, and a CI workflow cleanup landed today.
Read the issue →
May 17th, 2026 · 4 commits
Fixes a MePo ranking bug, adds expression hover message helpers, and restores correct pretty-printing under `pp.universes`.
Read the issue →
May 16th, 2026 · 7 commits
Performance and API work landed across elaboration, dyadic arithmetic, byte arrays, and module serialization, plus CI and build preset cleanup.
Read the issue →
May 15th, 2026 · 4 commits
Lean improves `lake shake --explain`, fixes `--plugin` parsing on Windows, and updates CI plus stage0 artifacts.
Read the issue →
May 14th, 2026 · 5 commits
Major config-eval refactor plus new lints, better instance errors, recursion-fix regression coverage, and structure-instance hover upgrades.
Read the issue →
May 13th, 2026 · 4 commits
ContextAsync race handling, try? testability, and clearer unused-variable warnings landed alongside a CMake fix for empty leanc args.
Read the issue →
May 12th, 2026 · 6 commits
Locale-aware time formatting, a safer server wait helper, and a TZDB search-path fix headline the day.
Read the issue →
May 11th, 2026 · 8 commits
+1
New local-time APIs, a safer `withSetOptionIn`, improved empty-`by` suggestions, and several bug/CI fixes land today.
Read the issue →
May 10th, 2026 · 6 commits
Lean adds HTTP serving for `trace.profiler` output and improves `grind` diagnostics; vector append lemmas now work across sizes.
Read the issue →
May 9th, 2026 · 2 commits
Lean4 made `Glob.ofString?` public and added CLAUDE guidance to avoid changing a PR’s GitHub base when rebasing locally.
Read the issue →
May 8th, 2026 · 3 commits
Lake now stores compiled configs in workspace-local paths, while CI pins a broken action tag to restore builds.
Read the issue →
May 7th, 2026 · 8 commits
+1
Major proof-engine upgrades landed: verifiable while/repeat loops, a new SymM-based mvcgen' tactic, plus deprecation-warning cleanup and runtime speedups.
Read the issue →
May 6th, 2026 · 14 commits
+3
Blockquotes now render in Verso docstrings, attribute loading gets stricter, LLVM 22 lands, and the runtime hardens OOM handling.
Read the issue →
May 5th, 2026 · 16 commits
+4
Renames `--clippy` to `--extra`, lets plugins declare init functions, and includes several fixes for termination errors, I/O, and crashes.
Read the issue →
May 4th, 2026 · 5 commits
UInt8 gets a clearer clamp API, scoped env exports are overhauled, and release tooling/CI are updated alongside benchmark script moves.
Read the issue →
May 3rd, 2026 · 7 commits
Lake now awaits extra deps before module headers and meta-import artifacts are fixed; `grind` gets several invariant and proof-hint fixes.
Read the issue →
May 2nd, 2026 · 7 commits
Better universe matching, safer default-instance visibility, and new `.instances` type-check diagnostics landed alongside a few Sym fixes.
Read the issue →
May 1st, 2026 · 2 commits
Docstring elaboration now rejects leaked metavariables consistently, and `grind`-based tactics stop wasting time on theory combination.
Read the issue →