Weekly
News about Lean, the theorem prover and programming language.
Leo de Moura, Chief Architect of the Lean FRO, presented "Lean: Machine-Checked Mathematics" at the Shanghai Institute for Mathematics and Interdisciplinary Sciences (SIMIS) on April 7, 2026. The slides, written in Verso, cover AI provers that use Lean, Mathlib, and grind, a proof-automation tactic inspired by modern SMT solvers.
Checked against: leodemoura.github.io
Leo de Moura merged pull requests adding Sym.Arith infrastructure for arithmetic normalization, fixing the sym canonicalizer, and adding a backward.isDefEq.respectTransparency.types option. An opt-in linter also warns about rfl simp theorems that only hold at higher transparency, part of a broader effort to ensure isDefEq respects transparency levels.
Checked against: lean4#13289lean4#13317lean4#13280lean4#13271lean4#13272lean4#13273lean4#13281
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
Leo de Moura opened a pull request enabling the backward.isDefEq.respectTransparency.types option by default, so the definitional equality checker respects the current transparency setting when matching metavariable types. The change prevents unintended unfolding of definitions and requires adding @[implicit_reducible] and @[expose] attributes to many library definitions.
Checked against: lean4#13283
In "Why Lean?", dated 2026-04-02, Leo de Moura argues that implementing Lean in Lean lets users extend it freely, and points to a small trusted kernel with multiple independent implementations. The post also names backward compatibility as Lean's weakness: Lean code written two years ago probably needs changes to compile today.
Checked against: leodemoura.github.io
The bundle tool creates self-contained Lean 4 bundles for teaching: students download a zip, unpack it, double-click "Start_Lean", and get a working editor with no installation, no network access, and no command line needed. Each bundle ships VSCodium with the lean4 extension and only the oleans the project needs.
Checked against: leanprover-community/bundle
In a post dated 2026-04-02, Leo de Moura argues that Lean's implementation in Lean itself underpins its extensibility, scalability, and soundness through a small trusted kernel. The post also names backward compatibility as Lean's weakness: code written two years ago probably does not compile today without changes.
Checked against: leodemoura.github.io
At Signal Shot Pre-Launch on April 1, 2026, Leo de Moura, Chief Architect of the Lean FRO, said Signal Shot will translate Rust to Lean via Aeneas, then prove correctness. The talk cited an AI-converted zlib, a C compression library, proved correct in Lean.
Checked against: leodemoura.github.io
Leo de Moura (AWS, Lean FRO) gave the talk "Lean: Machine-Checked Mathematics and Verified Programming" on March 30, 2026. The slides describe a general-purpose AI converting zlib (a C compression library) to Lean and proving the code correct, plus grind, a proof-automation tactic inspired by modern SMT solvers.
Checked against: leodemoura.github.io
The release changes reducibility handling: isDefEq no longer bumps transparency when comparing implicit arguments, and a new @[implicit_reducible] attribute and a backward-compatibility option ease migration. It also adds grind support for higher-order Miller patterns, mvcgen support for specifications in the local context, and faster startup.
Checked against: v4.29.0 release noteslean4 v4.29.0
CatCrypt provides a pipeline from Rust reference implementations, translated with the Hax tool, to security proofs in Lean, covering 172 cryptographic protocols and constructions (110 with the full Rust-to-Lean pipeline). Bas Spitters developed the whole library in two months working with GenAI.
Checked against: eprint.iacr.org
Patrick Shafto reported that the DARPA expMath kickoff included teams from CMU, Stanford, MIT, UCLA, Princeton and other universities, plus a panel of community supporters including Leo de Moura and the Lean FRO community, and Adam Topaz and the Mathlib Initiative.
Checked against: LinkedIn post
In "Lean 4 is the Greatest to Ever Do It", the author implements a small garbled-circuit evaluator using point-and-permute in Lean. The project combines a macro-based circuit syntax, OpenSSL bindings through Lean's C interface, imperative-style code, and a proof that the serializer behaves properly.
Checked against: markusde.ca
Ilya Sergey formalised and proved the correctness of the new borrow checker for Move, a smart contract language deployed on the Sui and Aptos blockchains: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant (Claude Code).
Checked against: proofsandintuitions.net
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
Leo de Moura gave an ETAPS tutorial on April 13, 2026, then an ETAPS Industry Day talk on April 15 covering Cedar (access control), SampCert (privacy), Strata (languages), Waimea (compiler), SymCrypt (crypto), Anneal (unsafe Rust) and Veil (distributed protocols), plus AI provers for which Lean is the training environment, evaluation harness, and deployment target.
Checked against: leodemoura.github.io
Mistral AI released Leanstral, with 6B active parameters and weights under an Apache 2.0 license. On FLTEval, a new suite built from pull requests to the FLT project, Leanstral pass@2 scores 26.3, beating Sonnet by 2.6 points while costing $36 to run versus Sonnet's $549.
Checked against: mistral.ai
In the blog post "Who Watches the Provers?", Leo de Moura notes that Claude (Opus 4.6) found seven kernel bugs in Rocq and two in Nanoda, a Lean proof checker written in Rust, but no proof of false in Lean's official kernel. The Lean Kernel Arena tests 7 kernels against 133 benchmarks.
Checked against: leodemoura.github.io
Menlo Ventures announced it is leading a $200 million Series A for Axiom at a $1.6 billion post-money valuation. Axiom trains systems to produce formally verified outputs in Lean, and Menlo Ventures describes the bet as one that Verified AI is a new paradigm.
Checked against: menlovc.com
Axiom Quant's Series A round, led by Menlo Ventures, values the startup at $1.6 billion. Axiom trains AI systems to generate formally verified outputs in Lean and plans to scale its training infrastructure and expand its team of math experts.
Checked against: siliconangle.com
A merged pull request by Henrik Böving ports the C emission pass from IR to LCNF. The PR describes this as the last step of the IR/LCNF conversion, enabling end-to-end code generation through the new compilation infrastructure.
Checked against: lean4#12781
Formalizing a 2006 paper on the stability of the two Higgs doublet model (2HDM) potential, using Mathlib and Physlib, revealed an error invalidating its main theorem. The paper calls this, to the best of its knowledge, the first non-trivial error in a physics paper found through formalization.
Checked against: arXiv:2603.08139
In Lean, structure field defaults can now depend on fields that come before and after them, and dotted function notation supports explicit mode (@.f) and explicit universes (.f.{u,v}). Field notation such as e.f.{u,v} now also accepts explicit universe levels, fixing a bug where levels were attributed to the wrong expression.
Checked against: lean4#12841lean4#13245lean4#13262
Math, Inc. used Gauss to help formally verify Maryna Viazovska's Fields Medal-winning sphere packing results, proving all remaining 8-dimensional results in 5 days and autoformalizing the 24-dimensional case in two weeks. The formalization grew from 70k to about 200k lines.
Checked against: math.inc