August 1st, 2026 · 5 commits
Selective `lake update` now rejects unknown packages, while kernel invariants were hardened and projection equality made stricter.
Read the issue →
July 31st, 2026 · 9 commits
Kernel checks got stricter around nested inductives and Prop detection, while `cbv at` returned with safe local-hypothesis reduction.
Read the issue →
July 30th, 2026 · 15 commits
+1
New do-notation assertions, faster vcgen framing, and multiple soundness fixes land alongside module export and contract syntax updates.
Read the issue →
July 29th, 2026 · 4 commits
Lean4 adds `where finally | spec` discharge blocks and generalizes `withSetOptionIn`, while tightening `cbv` and warning on useless init visibility.
Read the issue →
July 28th, 2026 · 5 commits
Lean4 patches a kernel soundness bug, teaches cbv stacked dependent projections, silences deprecated-syntax noise, and hardens rebootstrap CI.
Read the issue →
July 27th, 2026 · 12 commits
Lean 4 adds intrinsic do-loop contracts, surfaces linter code actions, fixes deprecated-module warning positions, and ships a parser cache speedup.
Read the issue →
July 26th, 2026 · 2 commits
Fixes a private-import initialization segfault and overhauls Lake inundation benchmarks with precompile variants.
Read the issue →
July 25th, 2026 · 2 commits
Linux shared libraries now ship SONAMEs, with Lake loading adjusted to keep precompiled imports working; CI also tightens one cache step.
Read the issue →
July 24th, 2026 · 11 commits
Lean4 tightened vcgen spec priorities and fixes, made Hoare triples universe-polymorphic, and removed a major instantiateMVars blowup.
Read the issue →
July 23rd, 2026 · 13 commits
+2
Lean’s HTTP stack gained redirect validation, body-stream error propagation, and RFC-compliant handling for bodyless responses, plus TSan support.
Read the issue →
July 22nd, 2026 · 17 commits
+4
A busy day: a kernel soundness fix, VCgen gains new splitting/spec handling, and floats now have logical Int conversions.
Read the issue →
July 21st, 2026 · 10 commits
+4
Lean4 added replayable HTTP bodies, expanded Float/Float32 APIs, and fixed several correctness bugs in tactics, parsing, replay, and runtime threads.
Read the issue →
July 20th, 2026 · 16 commits
+1
Lean4 adds stateful linter plumbing, fixes a vcgen annotation bug, improves grind homomorphism support, and tightens universe linting.
Read the issue →
July 19th, 2026 · 5 commits
Lean4 adds `grind homo_pred`, validates `grind homo` rules, and ships a broad set of homomorphism lemmas for numeric types and `BitVec`/`Fin`.
Read the issue →
July 18th, 2026 · 7 commits
Lean4 adds a new `@[grind homo]` attribute, plus fixes for `grind` performance and canonicalization bugs, and a private-export regression.
Read the issue →
July 17th, 2026 · 13 commits
Major vcgen and grind fixes land alongside a security-ish olean flush fix and a public exposure bug fix for inferInstanceAs.
Read the issue →
July 16th, 2026 · 14 commits
+2
Major Sym.simp and vcgen fixes landed alongside a new core-internal linter set and a few API cleanups.
Read the issue →
July 15th, 2026 · 14 commits
+1
Big day for automation and solver work: new trace postprocessing/storage, BitVec and cutsat fixes, plus incremental `set_option` elaboration.
Read the issue →
July 14th, 2026 · 11 commits
+2
Lean4 adds a `liaSteps` cap for `grind`, fixes a completeness bug in ring simplification, and lands new trace postprocessing support.
Read the issue →
July 13th, 2026 · 6 commits
Bootstrapping fixes for grind and BitVec, a clearer class-instance reducibility warning, plus a syntax borrow-annotation perf tweak.
Read the issue →
July 12th, 2026 · 3 commits
Three bug fixes harden `grind`: bitvector literal normalization, `0 ∣ p` handling, and a BitVec simproc crash/unsoundness fix.
Read the issue →
July 11th, 2026 · 7 commits
Lake fixes exe-template file generation and adds new dependency facets, while Lean trims costly instance checking and inlines unsafe terms better.
Read the issue →
July 10th, 2026 · 6 commits
Performance tweaks for grind and exporting, plus a new vcgen benchmark and a few test/doc cleanups.
Read the issue →
July 9th, 2026 · 13 commits
Performance wins for grind and instance synthesis, plus runtime and elaborator fixes for stack handling, partial_fixpoint, and deprecations.
Read the issue →
July 8th, 2026 · 10 commits
New hints for unused bindings and simp args, plus a major incremental-elaboration fix that avoids rerunning tactics on trailing whitespace changes.
Read the issue →
July 7th, 2026 · 19 commits
+3
Deterministic kernel recursion limits, SymM invariant enforcement, and a dependent do-`match` fix headline the day.
Read the issue →
July 6th, 2026 · 18 commits
+1
New `rw` for `sym =>`, better `finish?`, VCGen `mdata` handling, and several bug/perf fixes plus API cleanup.
Read the issue →
July 5th, 2026 · 2 commits
Lake now flushes config traces before truncation and falls back to reconfiguration when the trace is unreadable or invalid.
Read the issue →
July 4th, 2026 · 9 commits
New `sym` tactics and fixes land alongside a kernel-level `Fin.foldl` reduction, array in-place mapping, and key bug fixes.
Read the issue →
July 3rd, 2026 · 12 commits
+1
Major time-format rewrites, POSIX TZ parsing for future zone rules, and Lake API/archive improvements landed together.
Read the issue →