Weekly
News about Lean, the theorem prover and programming language.
Lean releases, the compiler, tactics, Lake, Verso, libraries, kernels, and checkers. 142 items, newest first.
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
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#15304lean4#15329lean4#15175lean4#15545
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
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
In Lean, an asynchronously elaborated theorem's exported info in a module is now available as soon as its signature is, instead of after its proof is elaborated. A second change stops modules from exporting constants such as foo.eq_1 realized only inside a proof, so such proofs no longer trigger downstream rebuilds.
Checked against: lean4#15559lean4#15563
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
A merged Lean pull request adds backward.grind.normalizer, which switches grind to the Sym.simp-based normalizer when set to false (the default behavior is unchanged). Related changes add grind_norm, a debugging tactic whose check mode runs both normalizers and fails when results differ, and fix negation-pushing rewrites that had been dead code since #9271.
Checked against: lean4#15464lean4#15375lean4#15378
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
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#15295lean4#15297lean4#15298lean4#15190
A merged pull request by Jason Reed adds a Publish button to the project summary when a workbench-publication.json file configures Verso builds. Clicking it runs a Verso build and serves the result on a route extending the project URL. A follow-up makes publications create temporary directories in roughly the same way as tracked commands.
Checked against: lean-workbench#139lean-workbench#149
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
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
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
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
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