Weekly
News about Lean, the theorem prover and programming language.
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
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
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
During an audit of the Miden VM, a zero-knowledge VM with its own assembly language, Trail of Bits had agents build a Lean model of the VM executor, producing 95 correctness proofs covering all binary arithmetic components of the core library. The work identified two subtle bugs that the existing unit test suite did not catch.
Checked against: blog.trailofbits.com
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
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
A Mathlib pull request by Kim Morrison adds a supply-chain audit step to the hourly update_dependencies.yml workflow, posting diffs, high-risk files touched and suspicious added lines for each changed dependency. The diffs come from paranoid-lake-update, which uses bare clones and git only, so nothing from upstream is executed.
Checked against: mathlib4#43911
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
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
The leanprover/hex repository bundles the released hex libraries for verified computational algebra in Lean 4, including LLL lattice reduction, integer polynomial factorization, graph canonical labelling via a formalization of nauty, and algebraic numbers. Each computational library is Mathlib-free, with Mathlib correspondence proofs in separate theory libraries.
Checked against: leanprover/hex
con-ron ports con-leche, an external Lean checker with a formal consistency proof, to Rust. It was written by AI under supervision from Joachim Breitner, and its Rust code is proven (partially) correct via an Aeneas-generated model, so checking a proof with both tools guards against compiler or runtime bugs.
Checked against: leanprover/con-ron
Two merged pull requests add Lean.Data.Html, a type of HTML forests aimed primarily at authoring HTML, with a renderer that produces a String, plus HTML-like syntax with an elaborator into that type. Companion downstream-lean4 pull requests adopt the type and syntax throughout supported packages.
Checked against: lean4#14935lean4#15002
XTX Markets announced $10mn to Lean FRO, a focused research organisation run by Convergent Research, and $10mn to the Mathlib Initiative, each covering core operating costs to 2030. XTX Markets says Lean provided the verification layer in the auto-formalisation of Fermat's Last Theorem.
Checked against: xtxmarkets.com
The multi-stage competition seeks faster algorithms for verified computation (using the Lean kernel to check computational results in a proof) across eight problems, including Fibonacci, prime counting, Rule 110, and SHA-256. Entrants prove each algorithm matches its specification; submissions close November 20, 2026.
Checked against: terrytao.wordpress.comcompetition.sair.foundation
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
Lean 4.34.0, released 2026-09-14, fixes three soundness issues found with AI adversarial testing and adds defensive kernel checks. bv_decide gets integrated with sym and grind interactive modes and is up to six times faster, linters can carry state across commands, and lake lint gains a --code-quality mode emitting machine-readable JSON.
Checked against: v4.34.0 release notes
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
Greg Brockman says OpenAI pointed Astra at its own systems until it ran out of vulnerabilities to find, putting 25% of its production engineers on defense. Greg Brockman added: "There are ideas, for example, formally verifying all of software, that are possible with AI."
Checked against: @a16z on X
In under two weeks, Certora built an experimental C-to-Lean pipeline and proved that the Clight (CompCert's C intermediate representation) model of zlib's 266-line inflate_table function is memory-safe and terminating. The proof, around 20,000 lines of Lean, was written almost entirely by LLMs, and the Lean kernel checked every step.
Checked against: certora.com
con-leche is an external checker for Lean, proven in Lean never to accept a proof of False, implemented and proven by Claude (Fable and Opus) under heavy supervision by Joachim Breitner at the Lean FRO. On the FLT proof by Anthropic, it accepted 1,044,222 declarations in 2 h 22 min wall time.
Checked against: leanprover/con-lecheleanprover.zulipchat.com
OpenAI said 10,000 autonomous AI agents found a singularity in the Navier-Stokes equations in three dimensions, with the result formally checked in Lean. Hours earlier, Tristan Buckmaster at New York University and Levent Alpöge at Anthropic reported Lean-verified proofs for three related results, including one for the Euler equations.
Checked against: quantamagazine.orgblog.computationalcomplexity.org
On a 1,000-module slice, adopting the module system and import minimization cut task-clock to 3,268 s (down 63.1%) and wall-clock to 140 s (down 86.3%). Sebastian Ullrich also released the proof as a single 1.01 GiB .olean download that can be run through lean4export for external checkers.
Checked against: hackmd.iofermats-last-theorem export
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
Working largely autonomously over 11 days, Claude wrote 13 million lines of Lean (over 5x the size of Mathlib, the principal community library) and proved 29,500 intermediate theorems. Kevin Buzzard compiled the code and ran comparator on it, and the full proof is on GitHub with a written walk-through.
Checked against: anthropic.comxenaproject.wordpress.comanthropics/fermats-last-theoremnature.com