Weekly
News about Lean, the theorem prover and programming language.
Edition 16: 10 items published for May 7 to May 14, 2026.
The leanprover/lean-workbench repository aims to provide familiar (VS Code with the Lean 4 extension) and novel interfaces to Lean online, giving each user an isolated Code Server instance inside a bubblewrap sandbox. The README warns the project is in progress and experimental, with a security audit forthcoming.
Checked against: leanprover/lean-workbench
A merged Lean pull request by Sebastian Graf gives the Sym-based mvcgen' feature parity with mvcgen, except +jp (join-point handling), at a cost of about 10% vcgen slowdown for cleaner user-visible VCs. A separate change adds whileM, which makes repeat/while loops verifiable with mvcgen.
Checked against: lean4#13578lean4#13209lean4#13672lean4#13582
Sebastian Ullrich's merged Lean pull request adds the Lake package option requiresModuleSystem: Lake then warns whenever a non-module-system file (one without a module header) imports a module of the package. A separate fix repairs code generation that broke with structures using private fields and types inaccessible in the current scope.
Checked against: lean4#13646lean4#13679
A merged pull request by Kim Morrison makes the transparency hierarchy none < reducible < instances < implicit < default < all, so @[implicit_reducible] annotations no longer have the side effects @[instance_reducible] has. A separate open pull request by Leo de Moura enables the backward.isDefEq.respectTransparency.types option by default.
Checked against: lean4#13637lean4#13283
In merged Lean pull requests by Leo de Moura, grind diagnostics now show local hypotheses used as E-matching theorems with their user-facing names and instantiation counters. A new grind option, genLocal, controls the maximum term generation for local theorems (for example, hypotheses) and defaults to 8, the same value as gen.
Checked against: lean4#13699lean4#13698
Compiled Lake configurations such as lakefile.olean now live in the workspace's .lake/config, removing a source of contention between workspaces sharing a dependency. Lake also now includes IR for a meta import's transitive imports, fixing "missing data file" errors with the artifact cache, and all Lake tests are re-enabled by default.
Checked against: lean4#13683lean4#13600lean4#13692
A demo chapter on x80.org previews foreign Rust references backed by a live language-server lookup: resolved references render a compact Rust source link and a grouped Rust code panel fetched from the location returned by rust-analyzer. A reference the language server cannot find is reported as unresolved, without a code panel.
Checked against: x80.org
Wojciech Nawrocki merged a Yjs-based collaboration server that syncs changes between clients, plus collaborative editing support in the vscode-workbench extension. A separate change makes it impossible for openvscode-server instances to make requests against other instances.
Checked against: lean-workbench#14lean-workbench#12lean-workbench#18lean-workbench#17
Leo de Moura, Chief Architect of the Lean FRO, gave the talk "Lean: Machine-Checked Mathematics and AI Collaboration" at the University of Washington on May 8, 2026. The slides open with a general-purpose AI that converted zlib (a C compression library) to Lean, passed the test suite, and proved the code correct.
Checked against: leodemoura.github.io
Leo de Moura, Chief Architect of the Lean FRO, spoke on May 12, 2026 at the Science x AI Summit in Palo Alto (May 12-13, in person and online). The slides, written in Verso, cover Mathlib, IMO-level AI provers using Lean, and verification work on Cedar and SymCrypt.
Checked against: leodemoura.github.iosair.foundation