Sep 7–13, 2026 · 64 commits
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 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
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
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
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
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
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
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
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
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
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
This week added VCGen framing and speedups, tightened parser/option behavior, improved Verso docstrings, and shipped several compiler/CI fixes.
Read the issue →