Weekly
News about Lean, the theorem prover and programming language.
In a LinkedIn post, Alexander Gerko says that over the last month he "vibe researched" several PhDs' worth of maths results in his former field, complete with Lean formalization, including a claimed counterexample to a top-5 major conjecture. Gerko predicts "50 years' worth of maths progress in the next 2 years."
Checked against: lnkd.in
Merged Lean pull requests by Sebastian Graf name the precondition clause of a def contract requires, pairing with ensures, let requires and invariant bind assertion arguments such as a state monad's state, and add an assert element to do notation that vcgen proves as a verification condition while doing nothing at runtime.
Checked against: lean4#14602lean4#14589lean4#14603lean4#14614
Ziyi Yang, Wenji Fang, Chen Chen, Zhiyao Xie, and Hongce Zhang present CircuitProver, an agentic Lean 4-based verification framework that translates hardware designs and natural language specifications into Lean 4 models and reuses verified lemmas across tasks. Across 63 tasks it proves all benchmarks, while a vanilla agent solves 92.1% of them.
Checked against: arXiv:2607.27259
Amazon is providing substantial, long-term financial support to the Lean Focused Research Organization (FRO), the team building Lean, which Amazon calls the single largest donation in the FRO's history. Amazon ties the investment to agentic safety and cites Lean-based verification in Policy in Amazon Bedrock AgentCore, SampCert, and AWS Neuron.
Checked against: amazon.scienceitpro.com
Leo de Moura presented "The Lean Theorem Prover: Design, Evolution, and Impact" at FLoC 2026 in Lisbon on July 26, 2026. Kim Morrison and Leo de Moura followed with a talk at IJCAR (Monday July 27 at 11:50 am) on grind, a new extensible tactic based on SMT techniques.
Checked against: leodemoura.github.io
In the QF_Bitvec division of the SMT-COMP 2026 Single Query Track, bv_decide reached a correct score of 2401 with zero errors, ahead of cvc5 at 2375 and Z3-GEX at 2229. Bitwuzla-MachBV led the division with 2495.
Checked against: smt-comp.github.io
In leanprover/lean4#14484, Patrick Hulin reports that the kernel does not reject free variables in opaque declaration bodies, letting an adversarial metaprogram prove False with no axiom dependencies. The report, largely generated with AI, suggests applying the closure check used for definitions and theorems, and the issue is now closed.
Checked against: lean4#14484
Alex Kontorovich announced the release of Tau Ceti, which Alex Kontorovich describes as the brainchild of Kim Morrison at the Lean FRO and a "Mathlib for AIs". The stated aim is to move fast and get a whole lot more formalized math than can be done at the scale of human review.
Checked against: @AlexKontorovich on X
Leo de Moura merged pull requests adding a [grind homo] attribute, since renamed [grind hom] and [grind hom_pred], and migrated the standard library to them. The new approach will replace the ToInt typeclasses used in grind. Andres Erbsen has already successfully tried and prototyped it.
Checked against: lean4#14446lean4#14468
Leo de Moura merged pull requests letting grind discharge hypotheses in conditional Sym.simp theorems, preventing grind timeouts on definitional equality checks for match-expression conditions, fixing a canonicalizer bug that made grind miss valid contradictions, and fixing grind dropping E-matching theorems from custom grind attributes.
Checked against: lean4#14425lean4#14444lean4#14439lean4#14426
A merged pull request by Jason (@jcreedcmu) enables per-message deflate compression for messages larger than 16MB in the websocket server behind lean4web, aiming to improve responsiveness of live.lean-lang.org. Full completions with Mathlib imported produce 20-40MB jsonrpc responses, which compress by a factor of 8-9x.
Checked against: lean4web#133
Son Ho's talk at the meetup, hosted by UTUM Venture Labs, previewed Formal Spec driven Development: AI implements a spec and generates its constraints using autoformalisation, while humans write the spec and check that the constraints cover it. Lean FRO's Munich-based team, including Head of Engineering Sebastian Ullrich, attended.
Checked against: LinkedIn post
The Lean developers published release candidate 1 for Lean v4.33.0, which centers on a more responsive editor, automatic try? proof suggestions, improved lia and grind tactics, a Float type that is no longer opaque, and kernel soundness fixes. It also 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-rc1
A merged Lean pull request by Paul Reichert makes whnfMatcher use the WHNF cache at sub-default transparency. It fixes a performance regression from #13895, merged on 2026-07-06, which enabled backward.isDefEq.respectTransparency.types by default as a breaking change that gives users more control over what is unfolded.
Checked against: lean4#14323lean4#13895
Leo de Moura merged pull requests that improve support for offsets in the SymM matcher/unifier, fix Sym.simp failing to rewrite terms containing unassigned metavariables (a failure reported by Sebastian Graf), and stop preprocessType in SymM from performing zetaDelta by default.
Checked against: lean4#14404lean4#14405lean4#14401
Merged pull requests extend vcgen, described as a verification condition generator over the Std.Internal.Do metatheory, with automatic frame inference and with loop invariants and def contracts (require and ensures clauses) that vcgen discharges automatically. A showcase repository collects imperative Lean programs verified with one 'vcgen ... with finish'.
Checked against: lean4#14389lean4#14195sgraf812/vcgen-showcaseleanprover/lean4
A merged Lean pull request adds a liaSteps configuration option to grind, meant to quickly interrupt the search for hard linear integer arithmetic problems. A second merged pull request implements grind propagators that evaluate BitVec operations on literals.
Checked against: lean4#14392lean4#14393
Lean v4.32.0 adds the do← marker for effect forwarding and cuts import Mathlib time by about 10% through a DiscrTree insertion fix. Lake's linting framework gains option-based control and module linters, and an experimental incremental-compilation mode lands behind CLI flags.
Checked against: v4.32.0 release noteslean4 v4.32.0
An open pull request by Sebastian Ullrich replaces hash maps built at import time with per-module prefix trees precomputed when oleans are written, cutting import Lean wall clock by 28% and mathlib's import phase by 21%, for about 6% larger stdlib oleans. A separate pull request by Sebastian Ullrich upgrading Lean to mimalloc 3 was merged.
Checked against: lean4#14362lean4#7786
A merged pull request lets linters persist and share state across command elaboration, with each stateful linter running an early phase and a late phase. Wojciech Różowski also changed the UnusedSimpArgs linter hint and split registerParametricAttribute as preparatory work for warning when @[deprecated] points at an already-deprecated declaration.
Checked against: lean4#14357lean4#14344lean4#14313
The first Hex packages provide dense matrices, row reduction, Gram-Schmidt, and a verified implementation of the LLL lattice basis reduction algorithm, plus a version that delegates computation to the C library fplll while verifying a certificate. Specifications are written first, then AIs implement code and proofs, and a blog post runs the Coppersmith attack on RSA.
Checked against: kim-em.github.iokim-em/hex
Lean now reuses tactic results when only whitespace after a tactic changes, so progress is kept when preparing to type the next tactic. The kernel's deep recursion error is now bounded by the maxRecDepth option instead of the physical stack size, which is a breaking change that may require explicit maxRecDepth bumps.
Checked against: lean4#13956lean4#11958
In a Logos Research prototype, a deterministic translator turns both the original and the rewrite into Lean, and a theorem prover proves the two compute the same result on every input. For iCPPI, a portfolio-insurance algorithm, the machine-checked proof ran to some 22,000 characters, with floats modelled as exact real numbers.
Checked against: logosresearch.ai
Merged pull requests by Leo de Moura implement the rw tactic and the case tactic (relevant for vcgen) in sym => mode, fix universe constraints and unresolved-instance reporting in SymM, add a hygienic parameter to intro-like functions, and speed up instance assignment when the goal type is ground.
Checked against: lean4#14287lean4#14278lean4#14277lean4#14280lean4#14279lean4#14330lean4#14314