Oct 26 – Nov 1, 2026 · 125 commits
Lean4 adds VCGen defaults, big grind speedups, and core APIs
This week Lean sharpened proof automation, sped up elaboration/kernel hotspots, and added new IO, arithmetic, and tooling APIs.
Read the issue →leanprover/lean4
Oct 19–25, 2026 · 104 commits
Lean 4 sharpens arithmetic tactics and speeds up the kernel
This week brings major `grind`/`lia` correctness and performance work, faster VC generation, cheaper imports, and kernel traversal optimizations.
Read the issue →Oct 12–18, 2026 · 58 commits
Lean 4 tightens core semantics and overhauls grind
This week brings safer recursion, stricter JSON/string behavior, faster runtime paths, and a large wave of `grind` and VCgen improvements.
Read the issue →Oct 5–11, 2026 · 71 commits
Lean4 adds HTML syntax, speeds imports, and hardens proofs
HTML snippets become first-class, while grind, vcgen, runtime, and import paths pick up correctness and performance fixes.
Read the issue →Sep 28 – Oct 4, 2026 · 66 commits
Lean4 hardens grind while expanding arithmetic and ground eval
This week brought major grind upgrades, new ground evaluation for chars, fins, and strings, plus a persistent typeclass cache.
Read the issue →Sep 21–27, 2026 · 84 commits
Lean4 adds major arithmetic power and hardens core caches
This week brought a new reflected arithmetic normalizer, faster and safer `grind`/`sym` tactics, and multiple runtime/cache correctness fixes.
Read the issue →Sep 14–20, 2026 · 57 commits
Lean4 ships verifier extensions and major performance wins
This week adds exception-aware specs, new float and modular arithmetic primitives, Lake tooling upgrades, and several elaboration/compiler speedups.
Read the issue →Sep 7–13, 2026 · 64 commits
Lean hardens verification and expands core runtime features
Weekly Lean4 update: external checker sandboxing, new runtime linearity markers, richer syntax/tactic ergonomics, and several kernel/runtime fixes.
Read the issue →Aug 31 – Sep 6, 2026 · 25 commits
Lean4 week: runtime fixes, faster elaboration, and Lake polish
Lean4 landed runtime crash fixes, elaboration and allocation speedups, new core lemmas, and finer-grain Lake precompile controls.
Read the issue →Aug 24–30, 2026 · 55 commits
Lean sharpens automation, SAT tooling, and runtime performance
This week adds new proof commands, expands bv_decide and SAT APIs, hardens challenge/checker flows, and trims runtime overhead.
Read the issue →Aug 17–23, 2026 · 70 commits
Lean hardens core safety while VCGen and Lake mature
Kernel and runtime safety fixes landed alongside a Bool-backed Decidable redesign, plus major VCGen, contract, and Lake workflow improvements.
Read the issue →Aug 10–16, 2026 · 59 commits
Lean4 ships faster proofs, safer kernel checks, and VCGen refactors
This week improved grind/vcgen performance, tightened kernel and instance search soundness, and added richer loop verification support.
Read the issue →