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
2026
← RecentSep 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 →Jul 13–19, 2026 · 70 commits
Lean4 lands new grind homomorphism support and VCgen upgrades
This week adds homomorphism-based grind reasoning, broader vcgen framing/spec handling, and several correctness and performance fixes across core.
Read the issue →Jul 6–12, 2026 · 76 commits
Lean 4 sharpens grind, fixes bitvectors, and tightens APIs
A week of solver and elaboration improvements, with key grind fixes, stricter kernel behavior, better IDE/lint UX, and Lake init changes.
Read the issue →Jun 29 – Jul 5, 2026 · 53 commits
Lean4 week: smoother proofs, faster internals, sturdier Lake
Core gains in list reasoning, tactic UX, timezones, and Lake reliability, plus several performance and soundness fixes.
Read the issue →Jun 22–28, 2026 · 53 commits
Lean 4 lands VCGen upgrades, parser fixes, and docstring polish
This week added VCGen framing and speedups, tightened parser/option behavior, improved Verso docstrings, and shipped several compiler/CI fixes.
Read the issue →Jun 15–21, 2026 · 59 commits
Lean 4 sharpens do-notation verification and float semantics
Major VCGen and `mvcgen` improvements, native float models, safer task/runtime handling, and a few Lake/CI fixes.
Read the issue →Jun 8–14, 2026 · 59 commits
Lean4 adds faster snapshots, stronger grind, and cache controls
This week brought big snapshot-loading gains, grind fixes and extensions, new do/mvcgen behavior, and Lake cache overwrite controls.
Read the issue →May 25–31, 2026 · 43 commits
Lean4 strengthens verification, linting, and runtime safety
This week added new tactic/combinator power, expanded VCGen and grind support, hardened linting, and introduced stricter build/runtime checks.
Read the issue →May 18–24, 2026 · 37 commits
Lean4 improves simplification, elaboration, and cache correctness
This week brought indexed-monad do notation, a new Sym.dsimp pipeline, faster string/dec paths, and several important elaboration and cache fixes.
Read the issue →May 11–17, 2026 · 38 commits
Lean4 sharpens time APIs, diagnostics, and editor tooling
A week of core Lean improvements: clearer time handling, faster elaboration/config code, sturdier tests, and better linting and hover support.
Read the issue →May 4–10, 2026 · 54 commits
Lean gets safer runtime, better diagnostics, and new verification tools
This week brought loop verification APIs, a faster experimental VC generator, improved diagnostics, and several safety and tooling fixes.
Read the issue →Apr 27 – May 3, 2026 · 16 commits
Lean4 fixes docs, instances, Lake builds, and grind
This week tightened docstring error reporting, instance visibility, Lake module setup ordering, and several grind correctness issues.
Read the issue →