August 31st, 2026 · 5 commits
Fixes a closure over-application crash, speeds up transparency switching, and adds a nicer Vector repr plus a new Int division lemma.
Read the issue →
August 30th, 2026 · 2 commits
App elaboration now preserves info trees and context for ambiguous syntax, while Lake’s primitive checker recognizes more builtins.
Read the issue →
August 29th, 2026 · 5 commits
Recursor printing and completions improve, while memory/layout and link-time fixes reduce friction and overhead.
Read the issue →
August 28th, 2026 · 11 commits
Lean 4 hardens `lake challenge`, adds BitVec min/max support, removes legacy native reduction, and fixes a `cbv` unfolding regression.
Read the issue →
August 27th, 2026 · 6 commits
Major CNF/LRAT refactor expands SAT APIs, `rwa` gets sane goal handling, and `leanchecker-paranoid` is slimmed down.
Read the issue →
August 26th, 2026 · 3 commits
New allocator-hardened leanchecker build, stronger symbolic Nat handling in bv_decide, and a major refactor of code-quality logging.
Read the issue →
August 25th, 2026 · 16 commits
+4
Lean4 adds safer DiscrTree access and fixes several elaboration/simp regressions, plus new strong induction support and deprecation hints.
Read the issue →
August 24th, 2026 · 12 commits
+1
New core syntax and bitvec APIs land alongside Nat.log2 evaluation, a Lake import fix, and several performance/robustness tweaks.
Read the issue →
August 22nd, 2026 · 3 commits
Lake adds a fail-fast build mode, while Lean improves structure field hovers and VCGen accepts registered WP instances.
Read the issue →
August 21st, 2026 · 12 commits
+1
Lean4 deprecates mvcgen, adds experimental vcgen controls, and lands notable correctness and build fixes across discrimination trees and Lake.
Read the issue →
August 20th, 2026 · 17 commits
+1
Lean tightened kernel/runtime safety, required newer GMP, and landed major VCGen and do-notation elaborator changes.
Read the issue →
August 19th, 2026 · 11 commits
Major Lean 4 work landed: new contract syntax, better VC variable names, a loop invariant refactor, and a kernel `is_prop` fix.
Read the issue →
August 18th, 2026 · 22 commits
+1
A mix of serious kernel soundness fixes, grind canonicalization work, and new verification/WP features landed today.
Read the issue →
August 17th, 2026 · 5 commits
A new `sym =>` tactic landed, LCNF got smarter about proof overapplications, and Lake now uses partial clones for dependencies.
Read the issue →
August 16th, 2026 · 1 commits
`grind`/`sym` now drain queued facts before splitting, cutting a worst-case `cases_next` benchmark from 5.9s to 0.11s.
Read the issue →
August 15th, 2026 · 2 commits
A breaking fix makes instance search respect expected types more strictly, plus a small docs typo cleanup.
Read the issue →
August 14th, 2026 · 11 commits
New VCGen splitting for `cond`, richer grind diagnostics, lower `bv_decide` latency, and an ST.Ref API/runtime fix landed today.
Read the issue →
August 13th, 2026 · 9 commits
Major VCGen namespace/module rework, better `vcgen` docs, a defeq heuristic change, and two runtime fixes: a borrowed-scalar leak and a performance regression.
Read the issue →
August 12th, 2026 · 12 commits
New `lift_lets`, incremental `bv_decide_push`, homomorphisms for `grind`, plus fixes for kernel timeouts, HEq handling, and inductives.
Read the issue →
August 11th, 2026 · 8 commits
Lean4 adds loop invariants/termination for `do`, speeds vcgen simplification, and improves `grind` support for loop measures and iterators.
Read the issue →
August 10th, 2026 · 16 commits
+5
Major updates span bv_decide CNF lowering, Lake cache/package handling, string extraction fixes, and a match elaboration optimization.
Read the issue →
August 9th, 2026 · 3 commits
Lake now treats cache corruption as non-fatal trace output and the leanExit test suite is less flaky about exit reporting.
Read the issue →
August 8th, 2026 · 1 commits
Lean4 now supports well-founded, state-dependent termination measures in `Spec.repeatM`, broadening vcgen's loop reasoning.
Read the issue →
August 7th, 2026 · 4 commits
Big Lean4 tooling update: bv_decide now integrates with grind, grind canonicalizes beta in types, and Lake cache tests were hardened for CI.
Read the issue →
August 6th, 2026 · 2 commits
Lake lint can now emit machine-readable code-quality results, and `ensures` clauses may use match alternatives with prettier formatting.
Read the issue →
August 5th, 2026 · 9 commits
New BVDecide type restrictions and several SymM/unifier fixes land alongside safer String.extract and contract/invariant elaboration improvements.
Read the issue →
August 4th, 2026 · 4 commits
New `forIn` specs cover effect-free containers, `bv_decide` now works in `sym` mode, and vcgen improves spec selection.
Read the issue →
August 3rd, 2026 · 6 commits
Major BVDecide performance work, a SymM theorem fix, and a Lake builtin-lint refactor; plus a small runtime and constant-folding optimization.
Read the issue →
August 2nd, 2026 · 5 commits
Lake now trims noisy exit-code and cache-transfer failures, library build errors are reported more precisely, and vector algebra proofs were de-automated.
Read the issue →
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 →