Weekly
News about Lean, the theorem prover and programming language.
Edition 25: 11 items published for Aug 6 to Aug 15, 2026.
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
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
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
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
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
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
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
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