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 →