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.
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
Julia Markus Himmel merged a change that compiles mimalloc as part of the Lean runtime, and Sebastian Ullrich moved rarely-updated Core.Context fields into a cold subobject (mathlib4: -0.82% instructions, -2.03% wall-clock). Lean also updated to mimalloc 3.4.5, fixing a Windows memory leak, and CI changes should halve merge queue run times.
Checked against: lean4#15017lean4#14982lean4#15060lean4#15123
A meta issue by Arthur Adjedj, worked out with @nomeata, plans kernel changes that move feature selection for inductives to the elaborator and aim for a decidable, transitive definitional equality algorithm. Recursive predicates like Acc would lose large elimination, and the kernel changes would ideally ship in a single release.
Checked against: lean4#14977
Arthur Adjedj's plan aims for a kernel that is easier to implement bug-free and to verify, with a decidable, transitive definitional equality algorithm and inductive features declared explicitly by the elaborator. Recursive predicates like Acc would lose large elimination, and kernel changes would ship in a single release.
Checked against: lean4#14977
Alex Meiburg's eink0rn, a clean-room Lean 4 kernel in Haskell generated mostly by Claude, was merged into the Lean Kernel Arena, which tests and benchmarks proof checkers for Lean. In the current round it answers all 72 invalid and 136 valid tests correctly and checks the mathlib test in 28.4 minutes.
Checked against: lean-kernel-arena#177arena.lean-lang.org
The roadmap covers lake check commands for external kernel checking, a code formatter, Nerodia (a Lean/Python FFI inspired by PyO3), and faster typeclass inference. It also covers the FRO's AI projects Tau Ceti, Hex, and Palomar, and defers investment in debugger infrastructure.
Checked against: lean-lang.org
Sebastian Ullrich merged leanchecker-paranoid, a variant of leanchecker built with allocator hardening, and lake challenge, a frontend to comparator that simplifies its setup. Joachim Breitner's lean-inductive-models performs translation validation of user-defined Lean inductives into an extensional type system with a small hard-coded inductive basis.
Checked against: lean4#14885lean4#14884nomeata/lean-inductive-modelsarena.lean-lang.org
The CSLib Initiative, a program of Renaissance Philanthropy, supports the growth of the CSLib open-source project (a focused effort on formalizing computer science in Lean) in the same way that the Mathlib Initiative supports Mathlib. Its site lists a team, a Strategic Advisory Board, and a roadmap of operational goals guiding its funding.
Checked against: cslib.io
The competition asks participants to improve the performance of verified computation in the Lean 4 kernel (the trusted component that checks every proof accepted by Lean) with optimized implementations and machine-checked proofs of correctness. Stage 1 pre-registration is open, with the official launch on September 15, 2026.
Checked against: @Leonard41111588 on XLinkedIn post
Wojciech Różowski merged a Lean pull request that generates strong_coinduct for coinductive_fixpoint predicates, strengthening coinduct, plus strong_induct for inductive_fixpoint ones. A second merged pull request adds a monotonicity_by clause so users can prove monotonicity of the underlying fixpoint functor with an explicit tactic block when automatic proof search fails.
Checked against: lean4#14855lean4#14861
Daniel Selsam used OpenAI internal models to find soundness issues in the official Lean kernel and runtime from July 30 to August 20, and Lean v4.33.1, released August 21, fixes all of them. Starting with Lean v4.35.0, lake check will export and recheck projects using lean4checker.
Checked against: leodemoura.github.io
Lean v4.33.1 is a patch release with runtime and kernel fixes, including soundness issues reported by Daniel Selsam (OpenAI) using OpenAI's internal models, and all users of v4.33.0 or earlier are encouraged to upgrade. Release candidate 2 for v4.34.0 was published the same day.
Checked against: v4.33.1 release noteslean4 v4.33.1lean4 v4.34.0-rc2v4.34.0 release notes
A merged Lean 4 pull request freezes objects whose 32-bit reference count overflows, preventing a use-after-free in the official kernel. The new logic is validated with a transliteration of its core to Lean followed by correctness proofs in a test file. Daniel Selsam (OpenAI) reported the issue using internal models.
Checked against: lean4#14838
A pull request by Robin Arnez, merged on 2026-08-20, changes Decidable p to a structure containing a Bool and a proof of either p or ¬p, giving more definitional equalities and letting the decide tactic stop carrying proofs. The breaking change was possible now that the new compiler is enabled.
Checked against: lean4#8309
A merged pull request by Mac Malone makes Lake fetch dependencies as treeless partial Git clones of a single revision, minimizing the amount of data downloaded. One caveat: Git operations inside a dependency, such as a git blame triggered by a VSCode extension, can cause lazy fetches.
Checked against: lean4#14782
A "Kernel bug hunt" document explains what counts as a Lean kernel soundness bug and how to validate a candidate before reporting it, using lake check, comparator (the validation tool) or its web interface. Starting with Lean v4.35.0, the distribution bundles four additional kernels, two of them formally verified.
Checked against: hackmd.io
Paul Reichert's merged PR ensures that, during instance search, metavariables for instance-implicit arguments are only assigned values of the expected type, fixing an issue Sebastien Gouezel hit while formalizing Riemannian metrics in Mathlib. A preparatory PR brought a clear performance improvement with no Mathlib breakage observed. Affected Mathlib declarations were fixed with a backward compatibility option.
Checked against: lean4#14624lean4#14583lean4#9077
Nerodia, a Lean/Python FFI library inspired by PyO3, uses Lake, Lean's build system, to build native Python modules in pure Lean and generates type stubs automatically. It is a work-in-progress with a very limited API, released primarily as a proof-of-concept and to obtain feedback on its design and build process.
Checked against: leanprover/nerodia
Two merged Lean pull requests by Sebastian Graf state each VERINA program's requires, ensures and loop invariants on the definition itself, for all 27 programs. A second pull request names a verification condition's variables after the program (acc, x instead of b✝), so proofs no longer need rename_i.
Checked against: lean4#14759lean4#14590
The merged pull request moves let/have declarations of the goal toward the root as far as dependencies allow. The new Sym.liftLets implementation is near-linear in the DAG size of the input term, running 680x faster than Meta.liftLets on a chain of 4000 lets and taking 85 ms for 32000.
Checked against: lean4#14768
The library, part of Hex, the computer algebra library for Lean, includes tactics for factorizing and irreducibility and implements van Hoeij's knapsack method, which according to Kim Morrison has never previously been formally verified. It builds on hex-lll, whose theory package proves that both lattice reducers satisfy their reducedness and lattice-preservation contracts.
Checked against: LinkedIn postleanprover/hex-lll
Merged pull requests let repeat and while loops state the invariant and termination measure that vcgen needs, so a loop inside a def with a contract verifies without manual proof steps. Other changes allow match alternatives in ensures clauses, invariants on destructuring for loops, and type ascriptions on contract binders.
Checked against: lean4#14703lean4#14701lean4#14682lean4#14686lean4#14669lean4#14685
Lean 4.33.0, published 2026-08-10, makes the editor more responsive, lets try? propose proofs on its own, improves the lia and grind tactics, and stops Float from being an opaque type. It also fixes kernel soundness bugs and enables backward.isDefEq.respectTransparency.types by default, the change most likely to need attention when porting.
Checked against: v4.33.0 release noteslean4 v4.33.0