Weekly
News about Lean, the theorem prover and programming language.
Papers, talks, courses, events, funding, and press. 53 items, newest first.
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
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
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
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
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
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
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
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
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
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
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
The new commitment brings the AI for Math Fund total to $31.5 million, with grants ranging between $100,000 and $1 million to support 12-24 months of work. Applications close on March 30, 2026 at 11:59 pm PT.
Checked against: renaissancephilanthropy.org
Kevin Hartnett's forthcoming book, "The Proof in the Code," tells the story of Lean's development and rise. The book is out in June, and pre-orders are open.
Checked against: @KSHartnett on X
In the blog post "Vibe-coding a debugger for a DSL", Joachim Breitner describes a small language embedded in Lean with a visual debugger in Lean's Info View and VSCode debugger support via the DAP protocol, built in one day of coding with GPT-Codex 5.3.
Checked against: joachim-breitner.de
Stephen Diehl built Kitty Cats, about 900 lines of Lean, with Anthropic's Opus 4.6 over two 30-minute sessions. The model handled the Yoneda lemma but needed guidance on multi-step rewrites and on refactoring verbose proofs. Diehl credits the lean-lsp-mcp server and the lean4-skills plugin for giving the model a feedback loop.
Checked against: stephendiehl.com
A post on shadaj.me, "Formally Verifying PBS Kids with Lean4," uses Lean to model the Cyberchase episode "Problem Solving in Shangri-La," a variant of Nim where players remove 1, 2, or 3 dragons. It proves the Cybersquad's poison-number strategy wins, introducing tactics such as rw, simp, split, and omega along the way.
Checked against: shadaj.me
In a LinkedIn post, Stan Fedotov argues the field is "moving towards automated verification in most domains," while noting Lean is "only useful when the standard library supports your field." In one paper, only a somewhat elementary part of the proof was verified in Lean, while the authors proved the deeper parts.
Checked against: LinkedIn post
Leo de Moura, Chief Architect of the Lean FRO, reviewed 2025 at Lean Together in January 2026: 12 releases, a new compiler fully implemented in Lean, and the grind proof-automation tactic. The talk also said 2026 will be the last year with significant changes to the language and standard library.
Checked against: slides (pdf)