PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:34Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:Lean since 2023}}		{{DISPLAYTITLE:Lean since 2023}}
			{{Lean theorem prover map}}
	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.		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.

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:15Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:Lean since 2023}}
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.<ref name="refhist">''The Lean Language Reference'', section 1.1 "History", for version 4.34.0 of Lean. https://lean-lang.org/doc/reference/4.34.0/Introduction/</ref> De Moura leads it as chief architect and Ullrich as head of engineering.<ref name="froabout">Lean FRO, "About" page, with its timeline "A Brief History of Lean" (read 14 October 2026). https://lean-lang.org/fro/about/</ref>

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.<ref name="frohome">Lean FRO, home page, "Vision" and "Mission" (read 14 October 2026). https://lean-lang.org/fro/</ref> 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.<ref name="roadmaps">Lean FRO, "Roadmap" (index of the roadmaps from August 2023). https://lean-lang.org/fro/roadmap/</ref><ref name="y41">Lean FRO, "The Lean FRO Year 4 - Part 1 Roadmap", covering September 2026 to February 2027. https://lean-lang.org/fro/roadmap/y4-1/</ref> In July 2025 Alex Gerko, founder of XTX Markets, announced gifts of $5 million to the FRO and $5 million to Mathlib.<ref name="rpgift">Renaissance Philanthropy, "Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of AI for mathematical research", 24 July 2025. https://www.renaissancephilanthropy.org/insights/lean-fro-and-mathlib-receive-10m-from-xtx-markets-founder-alex-gerko-to-further-advance-the-use-of-ai-for-mathematical-research</ref>

== 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.<ref name="firststable">"The first official release of Lean 4", Lean community blog, 8 September 2023. https://leanprover-community.github.io/blog/posts/first-lean-release/</ref> 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.<ref name="relnotes">''The Lean Language Reference'', "Release Notes", list of versions (read 14 October 2026). https://lean-lang.org/doc/reference/latest/releases/</ref> The Lean code in this edition is checked with version 4.34.1, of 24 September 2026.<ref name="relnotes" />

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.<ref name="rn422">''The Lean Language Reference'', "Lean 4.22.0 (2025-08-14)", release notes. https://lean-lang.org/doc/reference/latest/releases/v4.22.0/</ref>

The manual describes how <code>grind</code> 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 <code>bv_decide</code>, which calls an external SAT solver and checks the certificate it returns inside Lean.<ref name="grind">''The Lean Language Reference'', chapter 16, "The grind tactic", for version 4.34.0 of Lean. https://lean-lang.org/doc/reference/4.34.0/The--grind--tactic/</ref> The following example is the manual's, given a name so that its axioms can be printed:

<pre class="lean" style="background: #f8f9fa; border: 1px solid #c8ccd1; padding: 0.6em; margin: 0.3em 0; font-size: 0.85em; line-height: 1.35; overflow-x: auto; white-space: pre;">
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
</pre>

Lean 4.34.1 accepts the proof and prints <code>'no_solution' depends on axioms: [propext, Classical.choice, Quot.sound]</code>. 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 [[Lean theorem prover/System/Decision procedures|Decision procedures]] and [[Lean theorem prover/Explainers/Automation and its limits|Automation and its limits]]; the axioms at [[Lean theorem prover/Foundations/The three axioms|The three axioms]].

== Wider use ==

Mathlib kept growing; its history is at [[Lean theorem prover/History/Mathlib and its community|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.<ref name="froabout" /> They are described at [[Lean theorem prover/Applications/The polynomial Freiman-Ruzsa conjecture|The polynomial Freiman-Ruzsa conjecture]], [[Lean theorem prover/Applications/The Fermat's Last Theorem project|The Fermat's Last Theorem project]] and [[Lean theorem prover/Applications/The equational theories project|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.<ref name="alphaproof">Google DeepMind, "AI achieves silver-medal standard solving International Mathematical Olympiad problems", 25 July 2024. https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/</ref> Later work of this kind is described at [[Lean theorem prover/Applications/Machine learning and theorem proving|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.<ref name="sigplan">ACM SIGPLAN, "Programming Languages Software Award", recipients, 2025: Lean Theorem Prover. https://www.sigplan.org/Awards/Software/</ref> 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 theorem prover/History/Lean 1 to Lean 3|Lean 1 to Lean 3]].<ref name="skolemcade">CADE Inc., "Skolem Award", with the list of recipients (awards at CADE-30, July 2025). https://cadeinc.org/Skolem-Award</ref><ref name="skolem">University of Bonn, Department of Mathematics, "Skolem Award for Floris van Doorn", 27 May 2025. https://www.mathematics.uni-bonn.de/en/news/skolem-award-for-floris-van-doorn</ref>

== 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 <code>False</code>. 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.<ref name="rn4321">''The Lean Language Reference'', version for Lean 4.34.0, "Lean 4.32.1 (2026-07-22)", release notes. https://lean-lang.org/doc/reference/4.34.0/releases/v4.32.1/</ref>

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 <code>False</code> 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."<ref name="postmortem">Leonardo de Moura, "Postmortem for Kernel Soundness Bug #14576", 1 August 2026. https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/</ref> 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.<ref name="rn4322">''The Lean Language Reference'', version for Lean 4.34.0, "Lean 4.32.2 (2026-07-28)", release notes. https://lean-lang.org/doc/reference/4.34.0/releases/v4.32.2/</ref>

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.<ref name="postmortem" />

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.<ref name="y41" /> 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.<ref name="validating">''The Lean Language Reference'', "Validating a Lean Proof", for version 4.34.0 of Lean. https://lean-lang.org/doc/reference/4.34.0/ValidatingProofs/</ref> The reasons for this arrangement are set out at [[Lean theorem prover/Explainers/What has to be trusted|What has to be trusted]] and [[Lean theorem prover/System/Proof export and independent checkers|Proof export and independent checkers]].

<blockquote>
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 <code>grind</code> 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.
</blockquote>

== Next ==

[[Lean theorem prover/Applications/Research mathematics|Research mathematics]] · [[Lean theorem prover/Chronology|Chronology]]

== References ==
<references />

Lean theorem prover/History/Lean since 2023 - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source