June 30th, 2026 · 7 commits
Lake gains richer shared-library metadata and preloading support, while List.Perm picks up two useful nodup lemmas and CI gets adaptation fixes.
Read the issue →
June 29th, 2026 · 5 commits
Lean adds round-trip lemmas for `idxOf`, `finRange` ordering facts, and fixes `impossible`/grind goal handling, while reverting a parser tweak.
Read the issue →
June 28th, 2026 · 1 commits
Docstrings in macros now use the syntax tree’s format instead of local options, fixing Verso/Markdown mismatches across elaboration.
Read the issue →
June 27th, 2026 · 2 commits
Verso docstrings can now be elaborated from raw text when source positions are missing, fixing parameter references in more cases.
Read the issue →
June 26th, 2026 · 9 commits
Multiple grind performance tweaks land alongside a Verso docstring fix, new complete-lattice notation, and a C FFI flag export.
Read the issue →
June 25th, 2026 · 17 commits
+6
Major day for Lean4: doc rendering extensibility, `set_option in` parsing, float matching/equality, VCGen frames, and grind/perf fixes.
Read the issue →
June 24th, 2026 · 5 commits
New downstream adaptation PR automation lands, alongside a faster parallel lint script and a regression test.
Read the issue →
June 23rd, 2026 · 7 commits
+1
A new Lake feature lands alongside parser and `lia` fixes, plus CI/build cleanup and a cache-benchmark addition.
Read the issue →
June 22nd, 2026 · 12 commits
Lean4 renamed `mvcgen'` to `vcgen`, sped up VC/spec matching, and fixed codegen visibility handling for private constructors.
Read the issue →
June 21st, 2026 · 1 commits
Lean4 now ignores transient `_tmp_*` files during test globbing, preventing interrupted benchmark leftovers from appearing as phantom tests.
Read the issue →
June 20th, 2026 · 3 commits
Lean4 fixed a Lake remote URL bug, sped up test elaboration with shared header snapshots, and corrected a CI restart label.
Read the issue →
June 19th, 2026 · 13 commits
+2
New `WP` support for deep embeddings, a transparency split, a VCGen match fix, and a runtime/task race fix landed alongside perf and API work.
Read the issue →
June 18th, 2026 · 16 commits
+1
Lean4 added a dedicated `@[lia]` lemma set, exposed `Float`’s logical model, and fixed several runtime/concurrency issues.
Read the issue →
June 17th, 2026 · 9 commits
A new Float logical model lands alongside mvcgen fixes for specs, dependent lattices, and partial-correctness proofs.
Read the issue →
June 16th, 2026 · 10 commits
A big VCGen refactor lands alongside a new `Id` lift spec, an `IntX` clamp fix, and Lake module-system warnings/options.
Read the issue →
June 15th, 2026 · 7 commits
Nat.sqrt is upstreamed, Lake deduplicates artifact transfers, and the task-pool idle-thread change is reverted.
Read the issue →
June 14th, 2026 · 3 commits
Lake adds overwrite flags and prefers trace outputs, while Lean gains BitVec cpop/setWidth lemmas and Nat.reprFast folding.
Read the issue →
June 13th, 2026 · 2 commits
Lean4 adds BitVec.flattenList with lemmas and improves builtin assert docstring highlighting and parsing.
Read the issue →
June 12th, 2026 · 13 commits
Parallel snapshot loading, new grind disambiguation, and a handful of performance and bug-fix upgrades landed today.
Read the issue →
June 11th, 2026 · 16 commits
+4
Major grind correctness fixes, new incremental snapshot CLI flags, and several performance and Std.Internal.Do refactors landed.
Read the issue →
June 10th, 2026 · 8 commits
New `mvcgen'` syntax and VC flow control, plus a compacted-region refactor and a Bool constant-folding fix.
Read the issue →
June 9th, 2026 · 8 commits
Private namespaces now open correctly, WASM bool ABI mismatch is fixed, and do-elaborator diagnostics gain hoverable mutable vars.
Read the issue →
June 8th, 2026 · 9 commits
+1
Major do-notation semantics changed, env linters became option-driven, and the compiler gained USize constant folding.
Read the issue →
June 7th, 2026 · 2 commits
Lean4 overhauls its time API around the renamed DateTime type, while also exposing reflectBV for BVDecide users.
Read the issue →
June 6th, 2026 · 1 commits
A small performance tweak replaces a heavier object destructor with a more precise free path in refcount teardown.
Read the issue →
June 5th, 2026 · 4 commits
Major runtime, control-flow, and proof infrastructure updates landed, plus dependency/versioning cleanup in Lake.
Read the issue →
June 4th, 2026 · 6 commits
New whole-module syntax linters, builtin linter sets, Lake cache env overrides, plus deprecations and macOS test fixes.
Read the issue →
June 3rd, 2026 · 6 commits
Performance gains in DiscrTree and decidable quantifiers, a new PersistentHashMap.alter, and Lake dep resolution fixes.
Read the issue →
June 2nd, 2026 · 8 commits
+1
Lean4 adds ground-term evaluation for `Sym.dsimp`, fixes `rcases` info, and hardens the compiler and codegen against edge cases.
Read the issue →
June 1st, 2026 · 11 commits
+1
A major cleanup day: new do elaborator becomes default, bv_decide is refactored, and suggestion interspersing gets endpoint fixes.
Read the issue →