Week of May 7, 2026

Edition 15: 10 items published for Apr 30 to May 7, 2026.

Jonathan Protzenko uses Aeneas to verify bounds safety in jxl-rs

Jonathan Protzenko's case study uses Aeneas, a toolchain for verifying Rust programs through a functional translation to Lean, on jxl-rs, a Rust rewrite of the jpeg-xl codec. The proof shows an unchecked array access always stays within bounds and showcases recent Aeneas features, including official grind support and loop combinators.

Checked against: jonathan.protzenko.fr

Lean core May 7

Sebastian Graf merges experimental mvcgen' tactic into the Lean toolchain

The pull request adds mvcgen', reimplemented from the ground up on the new SymM-based framework for efficient symbolic evaluation. It will soon replace mvcgen and can outperform it by a factor of more than 100 on some synthetic benchmarks. Join point sharing and introduction of local specs are not yet supported.

Checked against: lean4#13644

Lean core May 1

Leo de Moura merges a series of grind fixes into Lean

The merged pull requests fix grind's AC invariants, a congruence-table panic, cast internalization order and missing proof hints. A new ringMaxDegree option (default 1024) bounds polynomial degree in the ring solver, and derived tactics such as lia, linarith and ring now fail quickly on out-of-scope problems.

Checked against: lean4#13593 lean4#13585 lean4#13590 lean4#13624 lean4#13625 lean4#13623 lean4#13614 lean4#13622

Lean core May 5

Leo de Moura fixes a panic and an assertion failure in Sym.simp

One merged Lean 4 pull request fixes a Sym.simp panic triggered when match reduction exposed kernel projection terms, for example in a do block with a for loop over tuple state. Another removes an incorrect assertion that failed on have-expressions whose binder type depends on an earlier binder.

Checked against: lean4#13635 lean4#13611 lean4#13612

Lean core May 3

Mac Malone extends Lean-to-Python module initialization in Nerodia

Mac Malone's merged pull request lets a Lean-written initializer add a constant to the Python module, adds Lean-side argument validation, and adds a Lean-to-Python-to-Lean test. A second merged change splits the global Python state (g_py_main) from the per-use GIL context (py_context).

Checked against: nerodia#3 nerodia#4

Lean core May 5

Wojciech Nawrocki adds a VSCode extension to lean-workbench

A pull request by Wojciech Nawrocki, merged on 2026-05-05, adds a VSCode extension to integrate it with the workbench in the leanprover/lean-workbench repository. The change also adds a launch target and server endpoint to debug the extension.

Checked against: lean-workbench#9

Lean core Apr 28

Wojciech Różowski moves Batteries linters into Lean core and extends lake lint

Wojciech Różowski upstreamed the dupNamespace and unnecessarySeqFocus linters from Batteries to core Lean as "clippy" linters, which are disabled by default and run with lake lint --clippy. lake lint --builtin-lint now also supports text linters, and a new script reports deprecated modules, options and syntax usage.

Checked against: lean4#13513 lean4#13538 lean4#13540 lean4#13586

Papers and events May 1

Leo de Moura presents machine-checked mathematics talk at Stanford symposium

Leo de Moura, Chief Architect of the Lean FRO, spoke on "Machine-Checked Mathematics in the Age of AI" at the Stanford Future of Mathematics Symposium on May 1, 2026. The slides, written in Verso, cover Mathlib's 270,000+ formalized theorems, Verso Blueprint, Comparator (a judge for Lean proofs), and Lean-based IMO medal AIs.

Checked against: leodemoura.github.io

Papers and events Mar 18

Leo de Moura presents Lean 4 at NASA Formal Methods Symposium

Leo de Moura, Chief Architect of the Lean FRO, presents "Lean 4: A Unified Platform for Programming and Verification" at the NASA Formal Methods Symposium on May 6, 2026. The talk covers grind, Lean's new proof automation, and industry verification work including Cedar, SampCert, and SymCrypt.

Checked against: leodemoura.github.io

Papers and events May 4

Nathanson publishes recording of talk about Aristotle's solutions

Nathanson has published the recording of a talk about Aristotle's solutions to problems, including the remark "I tried to figure out what it did that I didn't do to solve the problems." Pietro Monticone shared the video on X.

Checked against: @pietromonticone on X