Weekly
News about Lean, the theorem prover and programming language.
Edition 29: 15 items published for Sep 17 to Sep 24, 2026.
Using Aeneas, which extracts a pure model of Rust code in Lean, a 237 KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7 KLOC of Rust, including SHA-3 and ML-KEM ported from C. AI agents autonomously write proofs, which the Lean kernel independently verifies.
Checked against: arXiv:2609.15648
Markus de Medeiros, Ralf Jung, Lars Birkedal and nine coauthors explore how Lean features like flexible metaprogramming and quotient types can simplify the design and usage of Iris, providing a new implementation of the Iris proof mode with improved performance. Integration with Mathlib supports an application to probabilistic program verification.
Checked against: arXiv:2609.24252
Geby Jaff of Vals AI had 10 Claude Opus 5.5 agents coordinate on a message board; after about 15 hours and 733 messages they proposed C-HD, whose Lean proof (checked with the Lean Comparator tool) establishes a strict asymptotic improvement over n log n for a stated density of edges. The constants are enormous, so no practical speedup is established.
Checked against: vals.ai
Boris Cherny reports that a couple of short prompts to Opus 5.5 produced 16 PRs fixing various bugs and race conditions in the Claude Agent SDK. Boris Cherny also sometimes combines Lean and TLA+ to look for issues around data flow, concurrency, and state management.
Checked against: @bcherny on XLinkedIn post
Velvet 2.0 is now based on Lean's most recent verification machinery, is easier to set up and 10x faster, adding exception specs, ghost state and named proof goals. Vermilion, an experimental Lean 4 backend for the Verus Rust verifier, turns each obligation into a Lean theorem checked by the Lean kernel.
Checked against: LinkedIn postilyasergey/vermilion
Chunhao Liao, Hongxu Xu, Xintong Zhou, Yizhou Zhang and Chengnian Sun present Trivet, which verifies or refutes 147 of 148 LLVM transformations, including 60 loop-free transformations with symbolic bitwidths and 27 loop-containing cases. Every successful verdict is checked by the Lean kernel.
Checked against: arXiv:2609.19583
NASA Jet Propulsion Laboratory's PropertyKindCalculus formalizes René Dybkær's ontology on property, extended with Flater's tracking of kinds of quantities, and is described as the first in which the quantity calculus itself, beyond the taxonomy around it, is a checked artifact. It includes catalogues for eleven of the thirteen ISO/IEC 80000 parts.
Checked against: nasa-jpl/PropertyKindCalculus
FloatLib is a verified arbitrary-precision floating-point arithmetic library in Lean 4 that unifies IEEE binary and decimal arithmetic, arbitrary-width posits, P3109, and user-defined formats and rounding rules. Every certified backend is proved equal to a complete encoded specification, and the library, proofs, and benchmarks are released as open source.
Checked against: arXiv:2609.19352
lazylean, a C++ type checker for Lean 4, hands computing terms to a Krivine machine with call-by-need thunks, after Coq's cClosure. The Lean Kernel Arena, which tests and benchmarks proof checkers for Lean, lists lazylean 0.3.0 alongside checkers such as tenet 0.11.1, lean4cobol and nanoclo-fortran.
Checked against: corun1024/lazyleanarena.lean-lang.org
Lean Studio runs on macOS, Windows and Linux and re-checks every declaration from the compiled .olean files with Tenet, a separate implementation of Lean's type checker. Keith Adler's IDE also includes Prove It, which tries 17 tactics on any sorry at once, and an MCP server for AI assistants.
Checked against: keithadler/leanstudio
Kim Morrison opened a Mathlib pull request adding real_root_count, which checks an untrusted Sturm chain from Hex and shrinks the Abel–Ruffini archive file from 175 to 127 lines. A second pull request adds the leanprover/sos sum-of-squares tactic, where CSDP serves as a search oracle outside the trusted base.
Checked against: mathlib4#43512mathlib4#42336
A series of merged Lean pull requests adds Sym.Arith.normalize?, which rewrites ring and semiring terms into polynomial normal form with a proof by reflection, and an arith simproc for Sym.simp that uses it. Later changes extend it to relations, ring characteristic, non-commutative rings, and some field rewrites, and grind's ring solver now shares Sym.Arith code.
Checked against: lean4#15292lean4#15279lean4#15293lean4#15295lean4#15297lean4#15298lean4#15190
Leo de Moura's Commute repository combines a simproc (a metaprogram that simp calls on matching subterms) with realizable constants, so only the pairs proofs use are ever proved, avoiding a quadratic table of lemmas. A related Lean pull request by Sebastian Ullrich adds Environment.realizationEnvContains.
Checked against: leodemoura/Commutelean4#15237
David Thrane Christiansen's rewrite of the Verso docstring parser, a breaking change that tracks all details of the concrete syntax, was merged on 2026-09-18, and Verso has been adapted to it. Marc Huisinga has opened a pull request adding an extensible code formatter integrated with the language server.
Checked against: lean4#15064verso#989lean4#15218
Kim Morrison's lake samply command records a CPU profile of a Lean executable and serves it to Firefox Profiler, and Mac Malone added a copy option for path dependencies and split leanir code generation into a separate Lake job. Mac Malone also published Nerodia, a work-in-progress library for Lean/Python FFI inspired by PyO3.
Checked against: lean4#12545lean4#15142lean4#14906lean4#15231nerodia.lean-lang.org