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