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 →