Thursday, October 15, 2026
Lean WeeklyNews about Lean, the theorem prover and programming language.
Lean 4.35.0, published on 2026-10-12, adds vcgen, a faster and more general successor of mvcgen, plus lake check and lake comparator, which check a project with Lean's kernel and optionally several independent kernels now included in the toolchain.
Checked against: v4.35.0 release noteslean4 v4.35.0
Ziyang Qin, Yuan Liao, Ayush Khaitan, and Bennett Chow formalize the smooth three-dimensional Poincaré conjecture via Ricci flow with surgery and finite-time extinction. Together with the Moise smoothing theorem, the result yields the topological three-dimensional Poincaré conjecture.
Checked against: arXiv:2609.33842
The AI for Math Fund selected 22 applications representing 30 organizations from more than 470 submissions, bringing its total commitments to $35.1 million. Winners include TorchLean, a Lean-native framework for verified machine learning, and a project turning a Lean 4 visual proofwriting prototype into open-source infrastructure for reading AI-generated proofs.
Checked against: renaissancephilanthropy.org
Checked against: blog.trailofbits.com
Checked against: openai/mathopenai/math
Checked against: science.org
Checked against: dpwoodru/general-courtade-kumar-lean
Checked against: scottnarmstrong.comxenaproject.wordpress.com
SymCert, implemented in Lean, builds verified SMT-based analyses of Cedar policies, an open-source authorization language. In the FMCAD 2026 paper, five analyses used in a Cedar analysis service at Amazon Web Services were modeled and proved in one work day, and three extensions for new Cedar features took 4 to 8 days each.
Checked against: cdn.amazon.science
Flapjack is bringing the Pancake compiler, originally verified in HOL4, and its proofs to Lean, with a path compiling a fragment of Pancake to RISC-V where all stages except parsing and AST conversion have a correctness theorem. A MIPS32 backend targets the Ziren zkVM, but its output has been run only on Ziren's Lean model.
Checked against: flapjack-lang.dev
con-leche, a checker for Lean 4, comes with a proof in Lean that every environment it accepts has a model in set theory, so no accepted environment holds a proof of False. A new document gives a pen-and-paper account of that argument on a simplified fragment of the checker.
Checked against: leanprover.github.io
Google's launch post for Gemini 4 Argon (dated 2026-10-13) reports an arcsin implementation, a building block in recent quantum simulation algorithms, written by Argon and formally verified in Lean. It cuts spacetime cost by more than 100x compared to a published quantum CORDIC baseline.
Checked against: blog.google
Julia Markus Himmel redefined the order on String as the lexicographic order of its UTF-8 encoding, made Min Float follow the IEEE-754-2019 minimum operation, and added missing order instances for BitVec, List, Array, Vector and ByteArray. Sofia Rodrigues fixed leaks and refactored the libuv bindings.
Checked against: lean4#15581lean4#15257lean4#15274lean4#15304+3 more
A merged pull request by Sebastian Ullrich removes the limit of 255 object fields per constructor, and thus per structure. When a constructor has more, the compiler keeps the first 254 in the constructor object and stores the rest in a chain of spill objects, with one pointer followed per spill object on access.
Checked against: lean4#15516
Checked against: lean4#15559lean4#15563
Checked against: lean4#15464lean4#15375lean4#15378
Checked against: lean-workbench#139lean-workbench#149
A pull request by Sebastian Graf documents the vcgen tactic and its Std.WP framework, adds the tutorial "Verifying Imperative Programs Using vcgen", and moves the mvcgen chapter and tutorial to their own files. The Kraken project already uses vcgen to prove that FFmpeg's FMA3 dot-product loop, over two arrays that may alias, terminates without faulting.
Checked against: reference-manual#927zrlk/kraken
Two merged pull requests by Sebastian Ullrich keep type class resolution results for later commands and let queries differing only in free variables share a cache entry. Building Mathlib takes about 4% fewer instructions and 8% less wall-clock time, and spends about 16% less time in type class resolution.
Checked against: lean4#14369lean4#14316
Wojciech Nawrocki merged pull requests adding Lean.Data.Html, a type of HTML forests aimed at authoring HTML, with a renderer to String, plus HTML-like syntax and an elaborator into that type. Separately, Emilio Jesús Gallego Arias added optional VIR support and a small Lean-to-JavaScript client example on Lean 4.35 to Verso Blueprint.
Checked against: lean4#14935lean4#15002verso-blueprint#491
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
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
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#15295+3 more
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
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
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
