Lean (proof assistant)

• 1. Introduction

  ›

  Lean received the ACM SIGPLAN Programming Languages Software Award in 2025. The four recipients were Gabriel Ebner, Soonho Kong, Leo de Moura, and Sebastian Ullrich. The cited impact covered mathematics, hardware and software verification, and AI in the same sentence. That breadth is unusual for a single software project.

  Lean is a proof assistant, meaning a program that verifies mathematical reasoning step by step, accepting nothing it cannot check from logical first principles. It is also a functional programming language, built on the calculus of constructions with inductive types. Free and open-source, it lives on GitHub.

  The project started as the work of a single researcher at Microsoft Research. What that researcher built would eventually attract Terence Tao and Google DeepMind. It also drew a startup co-founded by Vlad Tenev and Tudor Achim, with the stated goal of reducing AI hallucinations.

• 2. From Experiment to Production

  ›

  Lean was launched in 2013, and its earliest releases were openly experimental. Those initial versions, later classified as Lean 1 and Lean 2, included support for homotopy type theory-based foundations. That support was eventually dropped.

  Leonardo de Moura, who developed Lean primarily while employed at Microsoft Research, continued the project after moving to Amazon Web Services. Significant contributions came from other coauthors and collaborators throughout the project's history.

  Lean 3 arrived on the 20th of January, 2017, and represented the first moderately stable version. It was implemented largely in C++, with some features written in Lean itself. After version 3.4.2, the team officially declared it end-of-life and shifted focus to a successor. Members of the Lean community kept the older version alive, releasing unofficial builds up to version 3.51.1.

  In 2021, Lean 4 was released as a full reimplementation. Rather than interpreting code directly, Lean 4 produces C code that is then compiled, enabling efficient domain-specific automation. It also introduced a hygienic macro system and improved procedures for type class synthesis and memory management. A key structural change moved the frontend and other core components out of C++. They were now implemented in Lean itself, making them available to end users to override or extend. Lean 4 uses the C++17 standard, and it is not backwards-compatible with Lean 3.

  In 2023, the Lean Focused Research Organization, or Lean FRO, was formed as a nonprofit. Its goals were to improve the language's scalability and usability and to implement proof automation. The FRO's formation followed years of community-led work, including a library project that had already begun turning pure mathematics into verified code.

• 3. Digitizing Mathematics

  ›

  In 2017, volunteers launched a community-maintained project to create a single, comprehensive Lean library called mathlib. The stated goal was ambitious: to digitize as much of pure mathematics as possible, reaching up to research-level results. All of it would live in one cohesive library. As of May 2025, mathlib contained over 210,000 formalized theorems and more than 100,000 definitions. In 2026, the library was awarded the Demailly prize for open science.

  Lean also maintains an official standard library called Std. It provides common programming tools: tree maps, hash maps, datetime functions, and concurrency primitives. A separate community-maintained collection called batteries extends that foundation with additional data structures, useful for both mathematical research and conventional software development.

  CSLib targets theoretical computer science; SciLean is designed for scientific computing applications. PhysLib's stated aim is to give physics the same comprehensive formal foundation that mathlib established for pure mathematics. Among the prominent mathematicians who adopted Lean for their own work are Thomas Hales, Kevin Buzzard, Terence Tao, and Heather Macbeth.

• 4. Four Researchers, One Tool

  ›

  Thomas Hales adopted Lean for a project he called Formal Abstracts. Kevin Buzzard, based at Imperial College London, built the Xena Project. The Xena Project aimed to rewrite every theorem and proof in the Imperial College London undergraduate mathematics curriculum in Lean.

  Terence Tao released a Lean companion to his textbook Analysis I, formalizing selected sections of the text. Heather Macbeth used Lean as a teaching tool, giving students instant feedback on the logical validity of each step they took in a proof.

  By 2021, the same verification capacity had enabled a research team to formally check a proof at the cutting edge of mathematical knowledge.

• 5. Proofs at the Frontier

  ›

  In 2021, a team of researchers used Lean to verify the correctness of a proof by Peter Scholze in the area of condensed mathematics. The project attracted significant attention for formalizing a result at the active cutting edge of mathematical research. Condensed mathematics was not historical work; it was being developed and debated at the time.

  In 2023, Terence Tao used Lean to formalize a proof of the Polynomial Freiman-Ruzsa conjecture. Tao and collaborators had published the result itself in that same year. The Polynomial Freiman-Ruzsa conjecture was one of the few results formalized in Lean at nearly the same moment it was discovered.

• 6. A Million Lines of Physics

  ›

  In 2025, Joseph Tooby-Smith used Lean to examine a paper published in 2006 on the stability of the Two-Higgs-doublet model potential. The formal check revealed an error. The paper had circulated for close to two decades before Lean caught what human reviewers had missed.

  Kevin Buzzard, at Imperial College London, had argued that formalization was already having a big impact on mathematics. He saw no reason theoretical physics could not be treated the same way. A library called PhysLib aimed at exactly this: a definitive formal repository for physics in Lean. 'Ideally, we need a million lines of physics, and that might be hard work to get,' Buzzard said. He predicted manual effort would dominate the early phase, before machines eventually took over.

  Artificial intelligence researchers, watching the same developments in formal verification, had come to their own conclusions about what Lean's formal structure could do for them.

• 7. AI Learns to Prove

  ›

  In 2022, OpenAI and Meta AI independently created AI models to generate proofs of high-school-level olympiad problems in Lean. Meta AI made its model publicly available alongside the Lean environment.

  Vlad Tenev and Tudor Achim co-founded a startup called Harmonic in 2023. Harmonic's stated aim was to reduce AI hallucinations by generating and checking Lean code.

  In 2024, Google DeepMind released AlphaProof. AlphaProof proved mathematical statements at the level of a silver medalist at the International Mathematical Olympiad. It was the first AI system to achieve medal-worthy performance on a math olympiad's problems.

  In April 2025, DeepSeek introduced DeepSeek-Prover-V2, designed for theorem proving in Lean 4 and built on top of DeepSeek-V3. The Lean FRO's goal of implementing proof automation, set in 2023, was now shared by at least four major AI research organizations.