Weekly
News about Lean, the theorem prover and programming language.
The CSLib contributing guide covers two pillars: formalising computer science as reusable infrastructure, and code reasoning about mainstream programming languages via Boole, intermediate representations, and VC generation. Contributors who use AI must explain which tools they used in the PR description, following the Mathlib policy.
Checked against: leanprover/cslib
The Lean project published v4.29.0-rc5, the fifth release candidate for the v4.29.0 release of Lean, on GitHub on March 5, 2026.
Checked against: lean4 v4.29.0-rc5
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
Gauss, a Math, Inc. reasoning agent built to formalize proofs automatically, produced over 200,000 lines of Lean code for Maryna Viazovska's 24-dimensional proof in two weeks, without a preexisting blueprint. The work follows the 8-dimensional formalization announced on February 23, which built on the Formalising Sphere Packing in Lean project.
Checked against: spectrum.ieee.org
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
Santosh Nagarakatte's group built FLoPS, which formalizes the upcoming IEEE-P3109 standard for low-precision floating-point arithmetic in Lean. The work found errors in the draft standard, which were reported to the working group and fixed, and established properties of algorithms such as Fast2Sum in the context of P3109.
Checked against: mathstodon.xyz
SmtLibDsl is a domain-specific language embedded in Lean 4 for writing SMT-LIB2 constraint programs, with backends including Z3, cvc5, Kissat, and CaDiCaL. Bitvector widths and enabled SMT theories are tracked at compile time, and Lean validates every decoded SAT model.
Checked against: palladin/SmtLibDsl
Leo de Moura's lean#12179, merged on 2026-02-16, stops isDefEq from raising transparency to .default for implicit arguments, a behavior that caused scalability problems in Mathlib. Kim Morrison advises downstream projects not to move to v4.29.0-rc1 yet, and a later PR documents the design rationale behind the transparency hierarchy.
Checked against: leanprover.zulipchat.comlean4#12179lean4#12561
Lean v4.28.0 adds a lightweight symbolic simulation framework that integrates with grind and enables verification condition generators, plus user-defined grind attributes, a solver mode for bv_decide, and a first_par combinator that runs tactics in parallel. The release landed 309 changes, including performance improvements in bv_decide.
Checked against: v4.28.0 release noteslean4 v4.28.0
LambdaClass described Truth Research ZK, which turns Lean 4 specifications into optimized C and Rust code with formal correctness guarantees, noting one axiom (applyIndex_tensor_eq) needed for the tensor product of permutations. A pull request by Kim Morrison, prepared with Claude Code, proves that axiom as a theorem.
Checked against: amo-lean#2blog.lambdaclass.com
The pull request stops isDefEq from raising transparency to .default when checking implicit arguments, which was creating scalability problems in Mathlib. The PR calls it a very disruptive change, reversible with set_option backward.isDefEq.respectTransparency false. Separately, Lean published the second release candidate for v4.29.0.
Checked against: lean4#12179lean4 v4.29.0-rc2
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 merged Lean 4 pull request lets grind's e-matching engine keep lambda arguments as patterns when pattern variables are applied only to distinct lambda-bound variables. Previously such lambdas were ignored during matching, which limited theorems about combinators like List.foldl that take a function argument.
Checked against: lean4#12483
A merged Lean 4 pull request by Leo de Moura caches isDefEqI results in Sym, since symbolic computation such as VC generators finds the same instances repeatedly. On the vcgen_deep_add_sub_cancel benchmark, speedups range from 30% to 37%, with goal_1000 dropping from 1663.1 ms to 1141.9 ms.
Checked against: lean4#12486
Leo de Moura merged a pull request stopping isDefEq from raising transparency to .default for implicit arguments, which was creating scalability problems in Mathlib (old behavior: set_option backward.isDefEq.respectTransparency false). A second pull request fixes the type class resolution cache for classes with output parameters.
Checked against: lean4#12179lean4#12286
Leo de Moura opened leanprover/lean4#12448, a pull request that refactors the grind and Sym modules using Claude-assisted code transformations as an experiment in AI-aided code maintenance. The pull request is marked "do not merge".
Checked against: lean4#12448
A Mathlib pull request by Kim Morrison changes OrderDual from a type alias to a one-field structure, which prevents defeq abuse between a type and its order dual and requires explicit toDual/ofDual wrapping at type boundaries. The pull request notes it was prepared with Claude Code.
Checked against: mathlib4#35125
In a February 9, 2026 post, Ilya Sergey walks through modelling, model checking, and proving the Dolev-Strong Floodset consensus protocol in Veil, VERSE lab's auto-active Lean-based verifier for distributed protocols. Veil's model checker Lace explored 54904 states, 362 of them distinct, and caught a deliberately introduced agreement bug.
Checked against: proofsandintuitions.net
The pull request, merged on 2026-02-05, ensures simp does not "simplify" instances by default, since doing so creates non-standard instances that cause problems in Mathlib. The old behavior can be retrieved with simp +instances, and the backward compatibility flag for dsimp also deactivates the change.
Checked against: lean4#12244
A merged pull request to leanprover/lean4 makes the type class resolution cache properly cache results for type classes containing output parameters. Output parameter arguments, and universe levels that only appear in output parameter types, are erased from the cache key to avoid cache misses.
Checked against: lean4#12286
In an article, Predictable Machines, Inc. explains why it chose Lean as the foundation for Predictable Code, saying Lean's combination of a programming language and a theorem prover makes it possible to formally verify that AI-generated code stays aligned with specifications as systems evolve.
Checked against: LinkedIn postpredictablemachines.com
A post titled "Calling Lean Functions As Python Functions" introduces leancall, a Python library for Lean-Python interop built on LeanInteract, which gives a Lean REPL as a Python library. Examples include a Lean controller balancing a gym cartpole environment and a Lean ray tracer displayed with Python plotting tools.
Checked against: philipzucker.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