Weekly
News about Lean, the theorem prover and programming language.
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
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#13593lean4#13585lean4#13590lean4#13624lean4#13625lean4#13623lean4#13614lean4#13622
At SViL 2026 at INRIA Paris on April 20, 2026, Leo de Moura presented SymM, a monad for symbolic simulation and VC generation (turning code and specifications into proof obligations). On one challenge it ran about 100× faster than MetaM, and a Velvet port beat Dafny on 24 of 27 benchmarks.
Checked against: leodemoura.github.io
Clift verifies C programs by lifting them into Lean 4, following the methodology pioneered by seL4's AutoCorres pipeline in Isabelle/HOL and adapting AutoCorres2's five-stage pipeline to Lean 4's type theory. The accompanying paper reports that Claude Opus 4.6 generated the vast majority of the code, with 1,698 theorems and 12 remaining sorry.
Checked against: paper (pdf)eisbaw/Clift
nanobruijn, an experimental Lean 4 type checker in Rust forked from nanoda_lib, keeps expressions as pure de Bruijn indices with shift-homomorphic caching, and type-checks all of Mathlib (670k declarations) with 0 errors and 0 timeouts. The code changes were written by Claude (Anthropic), directed by Joachim Breitner.
Checked against: nomeata/nanobruijn
The symposium, held May 1-2, 2026, opened with Leo de Moura of Amazon speaking on "Machine-Checked Mathematics in the Age of AI." Other talks included Clark Barrett on CSLib, a platform for AI-assisted formal verification in Lean, Kevin Buzzard on autoformalisation, and Maryna Viazovska on formalizing the sphere packing problem.
Checked against: events.stanford.edu
A merged pull request by David Thrane Christiansen adds a full-page search to Verso, accessed by pressing enter in the search field. The page shows more results, provides more context, and has more filtering features.
Checked against: verso#847
The new grind.ematch.diagnostics option tracks how E-matching theorem instances depend on each other, and a ringMaxDegree option (default 1024) bounds polynomial degree in the grind ring solver. Other merged pull requests fix beta reduction to respect the generation threshold, fix a kernel error for Nat casts to non-Int types, and extend the homomorphism demo.
Checked against: lean4#13558lean4#13585lean4#13560lean4#13453lean4#13532lean4#13520
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#13513lean4#13538lean4#13540lean4#13586
The paper describes how Maryna Viazovska's 2016 solution of the sphere packing problem in dimension 8 was formally verified in Lean in February 2026, with the final stages done by Math, Inc.'s autoformalization model Gauss. It discusses the techniques used, the collaboration between humans and Gauss, and remaining project objectives.
Checked against: arXiv:2604.23468
Alex Meiburg asked Aristotle to formalize a Z80 emulator, build an assembler, and write a BigNum GCD in about 80 assembly instructions, then verify it by modeling the whole CPU execution. After 14 rounds of submitting to Aristotle (without editing the prompt), the proof succeeded.
Checked against: leanprover.zulipchat.com
s2n-bignum is a collection of integer arithmetic routines in pure machine code for cryptographic applications, and each function ships with a machine-checked proof in HOL Light. The CSLib Community port, presented at INRIA Paris 2026, covers the ARM (aarch64) part first, with the first two tutorials completed.
Checked against: arademaker.github.ioatlas-computing-org/bignum
A pull request by Wojciech Różowski, merged on 2026-04-22, adds builtin environment linting support to Lake, accessible via lake lint flags such as --builtin-lint and --clippy. It also introduces two builtin linters upstreamed from Mathlib (defLemma and checkUnivs) and a builtinLint package configuration option.
Checked against: lean4#13431
Kyuhee Kim, Auguste Poiroux and Antoine Bosselut evaluate GPT-5 and DeepSeek-R1 on 303 first-order logic problems: GPT-5 fabricates axioms during proof generation, while DeepSeek-R1 mistranslates premises. Other papers introduce PRIME, a benchmark of 156 theorems annotated in Lean 4, analyze tool-augmented formalization agents, and formalize the Wu-Ritt characteristic set method.
Checked against: arXiv:2604.19459arXiv:2604.19000arXiv:2604.16538arXiv:2604.14912arXiv:2604.18882
The Beneficial AI Foundation, Signal, and the Lean FRO launched Signal Shot on April 20, 2026, at the Software Verification in Lean workshop in Paris, with a talk by Max Tegmark and others. Leo de Moura writes that the effort targets libsignal's Rust implementation, translated to Lean with Aeneas, Son Ho's Rust-to-Lean functional translator.
Checked against: leodemoura.github.iobeneficialaifoundation.org
The Beneficial AI Foundation is verifying the Signal protocol and its Rust implementation in Lean, a public project meant to show that formal verification of major applications is doable today. The plan proves security properties of a protocol model, then uses the Aeneas tool to translate Signal's Rust code to Lean and check it against that model.
Checked against: beneficialaifoundation.org
Lean Squad, a GitHub Agentic Workflow, proved 443 theorems for raft-rs with three human nudge comments for about $240, and 518 theorems for Cloudflare's quiche, where it found an Ord antisymmetry violation. It also proved 259 theorems for PX4-Autopilot and found 2 bugs. Every definition and theorem statement is AI written.
Checked against: dsyme.net
Talks from the one-day workshop at INRIA Paris on April 20, 2026 are on YouTube, including a talk presenting SymM, a new monadic framework for high-performance verification tools built on Lean, Son Ho on SymCrypt, and Karthikeyan Bhargavan on verifying cryptographic applications. Derek Sorensen's talk was not recorded, and slides were provided instead.
Checked against: beneficial-ai-foundation.github.ioleodemoura.github.io
The pull requests fix a bug where satellite solvers (lia, ring, linarith) in sym => interactive mode threw an internal error, prune goals assigned by isDefEq, stop Sym.intros from assigning a metavariable when it introduces no binders, and restore eta-reduction of Sym.simp patterns containing loose pattern variables.
Checked against: lean4#13472lean4#13474lean4#13451lean4#13448lean4#13452
A merged pull request by Marc Huisinga adds three commands (Find, Copy, and Insert Unicode Symbol) that search symbols by abbreviation or by symbol, making it easier to insert Unicode into non-editor dialogs. Copy and Insert are bound to Ctrl+Alt+\ depending on whether a text editor is focused.
Checked against: vscode-lean4#762
Nerodia is a library for Lean/Python FFI inspired by PyO3 that uses Lake, Lean's build system, and generates type stubs for editors. It has a very limited API and is released primarily as a proof-of-concept and to obtain feedback on its design and build process.
Checked against: leanprover/nerodia
A HackMD note proposes to "separate the cheap default from the expensive exploration": a default grind mode that is cheap, fast and fails quickly, plus explicit named tactics such as nonlinear_ineqs and fin_cases that users, grind?, or AI invoke to produce replayable scripts.
Checked against: hackmd.io
The leanprover/verso-blueprint package, for writing Blueprint documents in Verso, now publishes Verso ports of the FLT and Sphere Packing blueprints, while Noperthedron and Carleson sit outside the catalog on the retired 4.34 line. Emilio Jesús Gallego Arias's porting harness has a human use Codex CLI to carry out the porting work.
Checked against: leanprover/verso-blueprintejgallego.github.ioejgallego/leanblueprint-to-verso
Veil is an open-source multi-modal verification framework for distributed protocols, embedded in Lean. It combines symbolic and concrete model checking, SMT-based automated proofs, and interactive theorem proving in a single tool with foundational guarantees and in-editor feedback.
Checked against: lean-lang.org