September 30th, 2026 · 6 commits
Key `grind` regressions were fixed, along with new normalizer coverage and a small e-matching tuning pass.
Read the issue →
September 29th, 2026 · 11 commits
Char ground evaluation, faster ctorIdx codegen, better grind normalization, and a few Sym/BVDecide fixes landed today.
Read the issue →
September 28th, 2026 · 10 commits
Security-ish? no; but a major day for `grind`: new arithmetic normalizers, Nat relation simplification, hom fallback rules, and a binder-sharing fix.
Read the issue →
September 27th, 2026 · 21 commits
Major `grind`/`sym` normalization work lands alongside bit-vector support and cache fixes; environment tracking also got a big overhaul.
Read the issue →
September 26th, 2026 · 6 commits
`grind` learns new bit-vector homomorphisms, signed `signExtend` reasoning, and stronger arithmetic normalization in fields.
Read the issue →
September 25th, 2026 · 9 commits
New cache-dependency tracking powers a debug cache-hit validator, while partial fixpoint unfold lemmas get much faster.
Read the issue →
September 24th, 2026 · 11 commits
Security, tactic, and arithmetic improvements span grind activation fixes, vcgen/WP migration, and broader Sym.Arith support.
Read the issue →
September 23rd, 2026 · 10 commits
+4
Big math automation lands alongside RC overflow fixes, a DiscrTree refactor, and a few smaller ergonomics tweaks.
Read the issue →
September 22nd, 2026 · 17 commits
+5
Lean4 adds a reflected polynomial normalizer, fixes async cancellation/races, and tightens float and bitvector semantics.
Read the issue →
September 21st, 2026 · 10 commits
+1
Big perf work, a new CaDiCaL FFI, better defeq errors, and a fix for unsafe pointer-equality code.
Read the issue →
September 20th, 2026 · 7 commits
Elaboration and compiler replay are faster, proof quick-checking improves for recursors, and module linter handling moves earlier in the pipeline.
Read the issue →
September 19th, 2026 · 2 commits
Two performance fixes cut overhead in command processing and closure construction, improving large-file elaboration times.
Read the issue →
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 →