Lean theorem prover/History/Lean since 2023

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Since 2023 Lean has been developed by a non-profit organisation set up for the purpose, with a new version roughly every month. This page covers that organisation, the versions and the automation added to them, the growth of the work done in Lean, and two flaws found in Lean's kernel in July 2026, with the response to them. It describes the state of things in October 2026.

The Lean Focused Research Organization

In July 2023 Leonardo de Moura and Sebastian Ullrich launched the Lean Focused Research Organization (FRO), a non-profit within Convergent Research. It was supported at the start by the Simons Foundation International, the Alfred P. Sloan Foundation and Richard Merkin, and the Lean reference manual reports that it now has more than ten employees. De Moura leads it as chief architect and Ullrich as head of engineering.

The FRO states its mission as improving Lean's critical systems and guiding Lean towards long-term self-sustainability. Its listed areas of focus include scalability, usability, proof automation and documentation. It published a roadmap for each year of its work from August 2023. From September 2026 it moved to six-month roadmaps, saying that the field was changing too quickly to plan a year ahead. In July 2025 Alex Gerko, founder of XTX Markets, announced gifts of $5 million to the FRO and $5 million to Mathlib.

A version every month

Version 4.0.0, of 8 September 2023, was the first stable version of Lean 4. Its announcement planned a new minor version roughly each month, each preceded by a candidate version. The plan has held. The manual's notes list every version from 4.1.0 of 26 September 2023 to 4.35.0 of 12 October 2026, with occasional patch versions between them. The Lean code in this edition is checked with version 4.34.1, of 24 September 2026.

Version 4.22.0, of 14 August 2025, brought two large changes. The old compiler was replaced by a new one. And Lean gained grind, which its notes call an SMT-style tactic, with solvers for particular theories, among them a solver for linear integer arithmetic and one based on Gröbner bases.

The manual describes how grind works. Several engines share a common store of facts: congruence closure, constraint propagation, E-matching, guided case analysis, and solvers for linear integer arithmetic and commutative rings. Every proof it finds is by contradiction. Like other tactics, it produces ordinary Lean proof terms. For problems that are purely Boolean, the manual points instead to bv_decide, which calls an external SAT solver and checks the certificate it returns inside Lean. The following example is the manual's, given a name so that its axioms can be printed:

theorem no_solution (x y : Int) :
    27 ≤ 11 * x + 13 * y →
    11 * x + 13 * y ≤ 45 →
    -10 ≤ 7 * x - 9 * y →
    7 * x - 9 * y ≤ 4 →
    False := by
  grind

#print axioms no_solution

Lean 4.34.1 accepts the proof and prints 'no_solution' depends on axioms: [propext, Classical.choice, Quot.sound]. The search was done by the tactic; the term it produced was checked by Lean's kernel, and rests on Lean's three axioms and nothing else. How such procedures fit into Lean is described at Decision procedures and Automation and its limits; the axioms at The three axioms.

Wider use

Mathlib kept growing; its history is at Mathlib and its community. The FRO's timeline dates the start of several large collaborative projects: on the polynomial Freiman–Ruzsa conjecture in November 2023, on Fermat's Last Theorem in December 2023, and on equational theories in September 2024. They are described at The polynomial Freiman-Ruzsa conjecture, The Fermat's Last Theorem project and The equational theories project.

Lean also became a target for machine learning. In July 2024 Google DeepMind reported AlphaProof, a system that trains itself to prove statements in Lean. With a second system for geometry it solved four of the six problems of the 2024 International Mathematical Olympiad, for 28 points out of 42, the level of a silver medal. The problems were translated into formal language by hand, and some took the systems up to three days. Later work of this kind is described at Machine learning and theorem proving.

In 2025 Lean received two awards. The ACM SIGPLAN Programming Languages Software Award went to Lean, with Gabriel Ebner, Soonho Kong, Leonardo de Moura and Sebastian Ullrich named as contributors. Its citation mentions Mathlib at more than 1.6 million lines, the verification asked for by Peter Scholze, the polynomial Freiman–Ruzsa conjecture, and industrial uses, among them two at Amazon Web Services. The CADE Skolem Award, given for a paper from the Conference on Automated Deduction of ten years earlier that has passed the test of time, went to the 2015 system description of Lean, the paper discussed at Lean 1 to Lean 3.

Flaws in Lean's kernel, July 2026

Two versions of July 2026 each fixed a soundness bug in Lean's kernel. Version 4.32.1, of 22 July, fixed one by which a malicious metaprogram running in the same process as Lean's kernel could make it accept a proof of False. Its notes say that this opened no new line of attack, since such a program already has blunter ways to have bad proofs accepted, and that checking possibly dishonest proofs with comparator, described below, was not affected.

The second bug is the subject of a postmortem. On 25 July 2026 a purported "disproof" of the Collatz conjecture, produced with the help of AI, was published. It was not valid: it exploited a bug in the Lean kernel's handling of nested inductive types. On 28 July the exploit was reduced to a short proof of False and reported, and a fix was made within an hour. Leonardo de Moura's postmortem explains the bug. When an inductive type occurred nested inside another inductive type, parameters of the containing type that none of its constructors mention dropped out of an auxiliary type that Lean's kernel generates, so an ill-typed argument in that place was never checked. The bug could be reached only by metaprogramming, by sending the definition straight to Lean's kernel; Lean's front end would have caught the ill-typed term. The postmortem calls it "an implementation bug, not a hole in Lean's meta-theory." Version 4.32.2, of 28 July 2026, fixes it. Its notes add that this bug could be exploited even when proofs are checked with comparator, and advise users who must guard against malicious proofs to upgrade nanoda as well.

The same false proof had also passed a week-old version of nanoda, the main independent checker for Lean, written in Rust. That was a second, unrelated bug in nanoda, fixed a week before the Lean bug was reported. The postmortem draws the practical lesson. Checking with an independent checker still works, since this exploit needed two distinct bugs in two implementations, but users who rely on it need current versions of both. It also rejects the suggestion of restricting metaprogramming. The elaborator is untrusted by design, so soundness cannot depend on it refusing to produce a bad term, and Lean's kernel has to reject ill-typed definitions by itself. With help from an AI system specialised in security, further mistakes in Lean's kernel were found and fixed; nanoda caught all of them.

The FRO's roadmap for September 2026 to February 2027 makes independent checking a routine step. It plans commands for Lake, Lean's build tool, that re-check a development with the Lean kernel, with an alternative checker, or with every checker shipped with Lean, and it plans to include the comparator tool in Lean's distribution. The manual already calls comparator the gold standard against deliberately misleading proofs. It compiles the proposed proof in a sandbox, then replays it outside with Lean's kernel or an external checker, and confirms that the theorems proved are the ones stated in a trusted file. The reasons for this arrangement are set out at What has to be trusted and Proof export and independent checkers.

Provenance: the FRO's own pages, the Lean reference manual (history, version notes including those of 4.32.1 and 4.32.2, the chapter on grind and the section on validating proofs), de Moura's postmortem, the DeepMind announcement, the SIGPLAN and CADE award pages and the Bonn announcement were read on or before 14 October 2026. Dates of projects come from the FRO's timeline, which is the developers' own account. The postmortem names no version of Lean; the versions and dates of the two fixes come from the version notes. The one quotation is from the postmortem. Events after mid-October 2026 are not covered.

Next

Research mathematics · Chronology