Weekly
News about Lean, the theorem prover and programming language.
Edition 11: 13 items published for Mar 19 to Apr 2, 2026.
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
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
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
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
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
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
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
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
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
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
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
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