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 →
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 →