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 →
October 6th, 2026 · 14 commits
+2
A mix of important correctness fixes, two performance wins, and a few new syntax/VCGen capabilities landed today.
Read the issue →
October 5th, 2026 · 15 commits
+3
New HTML-like syntax lands alongside docstring parsing, grind, vcgen, and runtime/interpreter fixes.
Read the issue →
October 4th, 2026 · 17 commits
Multiple grind soundness fixes, a new Sym-based normalizer path, and major typeclass resolution cache work landed today.
Read the issue →
October 3rd, 2026 · 7 commits
Major grind upgrades: faster library-suggestion indexing, new Char/String handling, and more Fin homomorphism support, plus BVDecide private realizations.
Read the issue →
October 2nd, 2026 · 2 commits
`Sym.simp` now evaluates `Fin` literals/functions, and `grind` can solve certain equations in nonzero characteristic.
Read the issue →
October 1st, 2026 · 13 commits
+1
Lean gained an HTML forest type, a UF-capable bv_decide CEGAR path, and several new order/automation utilities.
Read the issue →