November 5th, 2026 · 24 commits
+3
Major fixes land across verification condition generation, kernel integer handling, typeclass caching, runtime deep copy, and HTTP/time APIs.
Read the issue →
November 4th, 2026 · 15 commits
+4
New safe pointer-equality helpers, VCGen and `grind` robustness fixes, plus HTTP URI/query handling and arithmetic normalization corrections.
Read the issue →
November 3rd, 2026 · 25 commits
+2
Major solver and elaborator improvements landed: float-literal defeq, better grind arithmetic, vcgen simp expansion, and Sym/join-point fixes.
Read the issue →
November 2nd, 2026 · 13 commits
Major updates to `grind`, `Sym.simp`, `bv_decide`, casts, and runtime/FFI behavior, plus a few test and CI fixes.
Read the issue →
November 1st, 2026 · 12 commits
New grind capabilities, multiple symmetry/universe fixes, and several interpreter/meta performance wins landed in one busy day.
Read the issue →
October 31st, 2026 · 7 commits
Major performance wins in `grind`, `rw`, and instance search, plus fixes for replay correctness and atomic Lake cache writes.
Read the issue →
October 30th, 2026 · 23 commits
+4
Major perf wins for bitvectors, strings, and hashing; new modular UInt64 and Nat.extendedGcd APIs; several fixes to Lake, time, JSON, and grind.
Read the issue →
October 29th, 2026 · 14 commits
+3
Major VCGen simplifications, a new atomic rename API, faster elaboration and grind, plus a new internal union-find.
Read the issue →
October 28th, 2026 · 20 commits
Major `grind` UX fixes, a new cache to cut quadratic inference costs, and several performance improvements landed today.
Read the issue →
October 27th, 2026 · 29 commits
+3
A feature-heavy day: new `vcgen` simplification defaults, JSON output for Lake checks, and several major theorem-proving performance wins.
Read the issue →
October 26th, 2026 · 20 commits
+1
New proof-folding LSP support, syntax deprecation via attributes, a vcgen simp attribute, and several correctness/perf fixes landed.
Read the issue →
October 25th, 2026 · 8 commits
Major kernel and grind performance work lands alongside a 32-bit static-data fix and broader literal support.
Read the issue →
October 24th, 2026 · 14 commits
Several performance wins for `lia`/`grind`, plus bug fixes for match conditions, process/syscall wrappers, and annotation cleanup.
Read the issue →
October 23rd, 2026 · 13 commits
Big performance work for `grind`, plus deprecation-syntax code actions and several core refactors/fixes.
Read the issue →
October 22nd, 2026 · 16 commits
Lean4 adds Nat-subtraction cancellation and fixes several grind/quotation/deprecation edge cases, plus a benchmark speedup.
Read the issue →
October 21st, 2026 · 14 commits
Major `grind`/`lia` fixes improve correctness, cut panic cases, and add smarter Cooper split handling plus a Cadical upgrade.
Read the issue →
October 20th, 2026 · 22 commits
+1
A day of substantial proof-engine work: `lia`/`grind` got multiple kernel-fix regressions handled, plus a new `vcgen +jp` mode.
Read the issue →
October 19th, 2026 · 17 commits
Key proof automation fixes land for subtype facts, funext candidates, and VC generation, alongside smaller Sym.simp and Lake improvements.
Read the issue →
October 18th, 2026 · 6 commits
Multiple fixes tighten `simp +arith` and `grind` normalization, preventing kernel loops and bad certificates around numerals, inverses, and forall binders.
Read the issue →
October 17th, 2026 · 8 commits
Lean’s `grind` gains subtype/eta fixes, mdata-safe intro handling, and a perf win from precomputed normalization theorems.
Read the issue →
October 16th, 2026 · 4 commits
Lean improves auxiliary-name lookup and fixes structural recursion on match discriminants, alongside a stage0 refresh.
Read the issue →
October 15th, 2026 · 10 commits
+1
New `vcgen` measure automation, private-name fixes, String/ByteArray order instances, and several grind/kernel regressions fixed.
Read the issue →
October 14th, 2026 · 10 commits
+2
Well-founded recursion is reworked around a non-eliminating fixpoint, while grind gets several correctness fixes around `<`, inverses, and inequalities.
Read the issue →
October 13th, 2026 · 10 commits
UTF-8 string semantics and lossy decoding improved, `grind` got a distrib option, and `lake shake` can enforce downstream imports.
Read the issue →
October 12th, 2026 · 10 commits
+1
Constructor fields over 255 now spill cleanly, JSON rejects duplicate keys, and release builds switch to stage2 binaries.
Read the issue →
October 11th, 2026 · 6 commits
Lean4 fixed several `grind` soundness/UX bugs, improved arithmetic normalization, and added more BitVec support.
Read the issue →
October 10th, 2026 · 9 commits
New grind parameter handling and replay fixes land alongside a major libuv runtime overhaul and a few solver correctness fixes.
Read the issue →
October 9th, 2026 · 15 commits
+1
A mix of important soundness, robustness, and performance fixes landed across grind, vcgen, async exports, and JSON handling.
Read the issue →
October 8th, 2026 · 6 commits
Performance wins for postponed codegen, plus fixes for equation-lemma determinism and a few correctness bugs in compiler/doc handling.
Read the issue →
October 7th, 2026 · 6 commits
Major safety fixes for timers/signals and a few performance and API cleanup changes landed alongside HTTP date compliance and String.toList migration.
Read the issue →