Weekly
News about Lean, the theorem prover and programming language.
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
Palomar, an initiative incubated by the Lean FRO and by ICARM, registers GitHub repository snapshots after checking with the Lean tool Comparator that proofs match the claimed statements, and with a large language model that the informal description matches. Terence Tao stresses that Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.com
Palomar, a public, searchable registry of machine-checked Lean formalizations incubated by the Lean FRO and ICARM, is now open for submissions, Terence Tao announced. Submitted repository snapshots are checked mechanically with the Lean tool Comparator and by a large language model, though Palomar is not a peer-reviewed journal.
Checked against: terrytao.wordpress.comLinkedIn post
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
Predictable Code uses Lean 4 formal verification to prove that AI-generated code matches specifications, and is currently in private beta. Predictable Machines also open-sourced lean4-json-schema, which derives JSON Schemas from types and proves at compile time that serialization always validates, and lean4-tree-sitter, typed bindings for tree-sitter.
Checked against: predictablemachines.comcode.predictablemachines.com
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
Researchers including Kaiyu Yang, Soonho Kong, Jingxuan He, and Dawn Song introduce Vero, a benchmark of 43 multi-module instances sourced from real-world repositories, each a multi-module Lean 4 repository with predetermined API interfaces. The strongest agent fully solves only 27 of 43 instances.
Checked against: arXiv:2608.13522
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
An unreleased research version of Claude increased the lower bound for the fraction of Riemann zeta zeros satisfying the Riemann hypothesis from 41.6% to 67.2%. Claude and Eric Easley produced a Lean formalization that passes comparator, the validation tool originally developed by Lean FRO with feedback from the AIMO team.
Checked against: anthropic.comanthropics/zeta-23-leanleanprover/comparator
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
On The Peterman Pod, Leo de Moura discusses how formal verification and proof assistants work, Lean's role in recent math results, when software is worth formalizing, and how LLMs plus Lean will change writing software and doing math. The episode is on YouTube, Spotify, and Apple Podcasts, with a transcript.
Checked against: @ryanlpeterman on XLinkedIn post
Lake now demotes cache failures during a build to trace-level messages, so builds run with --wfail or --iofail do not fail solely due to the cache, and lake cache get gains --package to fetch outputs for a specific workspace package. A new test mocks remote cache transfers with a mock Python HTTP server.
Checked against: lean4#14720lean4#14724lean4#14700
A graph on speed.lean-lang.org tracks mathlib4 build instructions over 25,000 commits, scaling older values to line up with newer ones across the move from the old speedcenter to radar and the switch to measuring only userspace instructions. Dashed lines mark the 90 toolchain bumps.
Checked against: speed.lean-lang.org
Arnav Mehta of Pramaana Labs reports that the company's system, which translates each question from English into Lean and then proves it, solved all 6 IMO 2026 problems in under 7 hours for less than $150. Pramaana Labs earlier announced $27 million in seed funding led by Khosla Ventures.
Checked against: lnkd.intechcrunch.com
LeetProof is an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean, that generates a program, its formal specification, and a machine-checkable proof from a natural-language description. The paper, accepted to ASE'26, reports that property-based testing validates specifications before any code is synthesised.
Checked against: arXiv:2604.16584lnkd.in
CSLib, the Lean Computer Science Library, now includes a proof of the FLP (Fischer, Lynch and Paterson) result: consensus is impossible in a distributed system with a faulty process and asynchronous messaging. Ching-Tsun Chou formalised the constructive pen and paper proof by Hagen Völzer from 2004.
Checked against: lnkd.inleanprover/cslib
Tim Sweeney called the response "an exemplary handling of a bug in the Lean theorem prover and proof verifier kernel." The bug was discovered in an AI generated proof, a contributor simplified it down to a straightforward reproduction, and the team fixed it speedily.
Checked against: @TimSweeneyEpic on X