September 18th, 2026 · 13 commits
Major docstring, contract, and Lake changes landed, alongside a recursive-elaboration performance fix and several API renames.
Read the issue →
September 17th, 2026 · 6 commits
+1
Major Lake dependency and profiling additions, plus AIG/CNF refactor and a BVDecide speedup.
Read the issue →
September 16th, 2026 · 4 commits
Grind arithmetic got a shared instance path and faster ring classification; release tooling also now ships Rust checkers that run outside CI.
Read the issue →
September 15th, 2026 · 14 commits
+4
Major Lean core work landed: exception-channel framing, lazy library suggestions, ChoiceResolutionInfo, new powMod/Fin exponentiation, plus several runtime and Lake fixes.
Read the issue →
September 14th, 2026 · 11 commits
New Lake options for export loading and sandboxing, plus Float/Float32 fused multiply-add support and a parser whitespace fix.
Read the issue →
September 13th, 2026 · 5 commits
Lake can now track and upload outputs for specific packages, comparator gets a default config path, and LRAT RUP accepts redundant hints.
Read the issue →
September 12th, 2026 · 1 commits
Lean4 tightens libuv refcounting and shutdown semantics, fixing promise ownership bugs and improving error reporting.
Read the issue →
September 11th, 2026 · 17 commits
+1
Erased variables land in do-notation, `lia`/`grobner` gain inline params, and the compiler gets several bug/perf fixes plus a new external checker.
Read the issue →
September 10th, 2026 · 13 commits
Lean 4 bundles nanoda and lean4lean, broadens kernel-reduction support for arrays/vectors, and fixes a goal-view regression plus arity reduction.
Read the issue →
September 9th, 2026 · 11 commits
Major changes to lake challenge isolation, compiler floating safety, export checking, plus new order/linear instances and goal-view fixes.
Read the issue →
September 8th, 2026 · 15 commits
+2
Major runtime/compiler fixes plus new linearity and range-syntax features, with an HTTP keep-alive bug fix and stronger kernel checking.
Read the issue →
September 7th, 2026 · 2 commits
Lean4 now has `lake check` and `leanchecker --from-export` to replay exports through the kernel, expanding external verification support.
Read the issue →
September 5th, 2026 · 2 commits
New Lake flags split import precompilation from full library builds, and a bugfix now applies server options inside packages too.
Read the issue →
September 4th, 2026 · 8 commits
Lean4 adds new parser/linter helpers, a missing `Decidable` instance, and a performance-oriented `Core.Context` refactor.
Read the issue →
September 3rd, 2026 · 4 commits
Heartbeat/mimalloc allocation is fused for speed, lazy RC is removed, and new intersection-emptiness symmetry lemmas land across Std.
Read the issue →
September 2nd, 2026 · 4 commits
New mergeSort lemmas and an opt-out for redundant termination warnings headline the day; a couple docs/process nits round it out.
Read the issue →
September 1st, 2026 · 2 commits
Dyadic comparison lemmas were renamed for correctness, and lake’s generated templates now use a newer checkout action.
Read the issue →
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 →