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 →leanprover/lean4
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 →Aug 3–9, 2026 · 29 commits
Lean4 sharpens bv_decide, vcgen, and Lake tooling
This week brought faster and more flexible bitvector automation, richer vcgen specs/termination, plus sturdier Lake lint and cache handling.
Read the issue →Jul 27 – Aug 2, 2026 · 55 commits
Lean hardens the kernel while expanding verification syntax
A week of major verification upgrades, several soundness fixes, and sharper tooling across cbv, lake, and linting.
Read the issue →Jul 20–26, 2026 · 71 commits
VCGen got much stronger, with key runtime and HTTP fixes
Lean gained safer VC generation, a kernel soundness fix, better HTTP/IO behavior, faster metavariable instantiation, and Linux linking improvements.
Read the issue →