Weekly
News about Lean, the theorem prover and programming language.
Formal Frontier is a new project focused on responsible, scalable, and open-source AI-driven autoformalization of mathematics, with XTX Markets supporting it. Its initial phase covers a community autoformalization specification, open-source tooling, and autoformalized texts chosen to fill gaps in Mathlib's existing coverage.
Checked against: mathlib-initiative.org
The leanprover/hex repository installs the released hex libraries at a single pinned set, including HexLLL for LLL lattice reduction and HexBerlekampZassenhaus for integer polynomial factorization. Each computational library is Mathlib-free, with Mathlib correspondence proofs in a separate theory library.
Checked against: kim-em/hex
A merged pull request by Kim Morrison separates the levels so that @[implicit_reducible] annotations no longer have the side effects @[instance_reducible] has, such as allowing type class search to see through marked declarations. The hierarchy is now none < reducible < instances < implicit < default < all, and a new with_implicit tactic is added.
Checked against: lean4#13637
In a series of merged pull requests, Leo de Moura built infrastructure for a dsimp in SymM, functions for simplifying binders, reusable reduction DSimprocs (beta, zeta, zetaAll, dsimpProj, dsimpMatch), and syntax for declaring dsimp variants. The last pull request implements the dsimp tactic for interactive sym => mode.
Checked against: lean4#13857lean4#13823lean4#13824lean4#13825lean4#13854
The merged pull request adds impossible by t, which uses the tactic t to prove that the current goal is impossible, closing the original goal as if sorry were used. try? gains an impossible branch that runs impossible by decide, impossible by simp, and impossible by grind in parallel.
Checked against: lean4#13771
Talos provides a Wasm interpreter optimized for reasoning plus a WP calculus layer for proving program properties, with a proof that the num-integer crate's gcd using Stein's algorithm is correct. The early-stage project aims for full Wasm coverage by passing the official testsuite, and verification of any Rust crate that compiles to Wasm.
Checked against: leanprover.zulipchat.com
A merged pull request adds Lean.CompactedRegion.save and read, which save or load one module at a time with explicit sharing, generalizing the batch saveModuleDataParts API. Separate pull requests by Sebastian Ullrich make Lean's CI build everything with Lake and fold the Linux Lake job into the Linux release job.
Checked against: lean4#13185lean4#13721lean4#13759
A merged Lean pull request by Kyle Miller adds a tactic configuration system that supports custom configuration syntaxes, and on a simple benchmark configuration evaluation takes 6.2% of the time it used to. A separate pull request by Kyle Miller makes InfoView hovers include information about specific metavariables.
Checked against: lean4#13651lean4#13446
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
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 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
The sos tactic is a sum-of-squares decision procedure for nonlinear real arithmetic, closely following John Harrison's HOL Light implementation. It calls the CSDP semidefinite programming library and rebuilds a fully certified result in Lean. Kim Morrison calls it a prototype and notes that frontier models have become very good at Lean metaprogramming.
Checked against: kim-em.github.ioLinkedIn post
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
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
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
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
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
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
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
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
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#13635lean4#13611lean4#13612
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
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
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).