Lean
In plain wordsA programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
An open-source proof assistantinteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong. that doubles as a functional programming language: definitions, theorems and proofs are all written as code, type-checked against a dependent type theory (a version of the calculus of inductive constructions) and certified by a small trusted kernel. Lean 4, a reimplementation written largely in Lean itself and compiled to C, serves both as a proof assistant and as a general-purpose language whose extensible syntax and tactic framework let users build their own automation. Its community library Mathlib, begun in 2017, is a large unified body of formalized mathematics (about 290,000 theorems and 140,000 definitions as of October 2026). Because a Lean proof either checks or fails, Lean supplies the verifiable reward signal for AI provers such as AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time. and DeepSeek-Prover and is the usual target language of autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify..
The model's argument looked convincing, but it only counted once it compiled in Lean.
Origin
Launched in 2013 by Leonardo de Moura at Microsoft Research; Lean 3 followed in 2017 and Lean 4 in 2021 (first stable release, September 2023). Mathematicians took notice when the Liquid Tensor Experiment (2020–2022) verified a central theorem of Peter Scholze's condensed mathematics. The nonprofit Lean Focused Research Organization was founded in 2023 to steward development.
Usage note
Not an acronym. 'Lean' now usually means Lean 4; Mathlib was ported from Lean 3 in 2023. The developers received the 2025 ACM SIGPLAN Programming Languages Software Award for Lean's impact on mathematics, verification and AI.
Related
- interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong.
- RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify.
- AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time.
- reinforcement learning with verifiable rewardsreinforcement learning with verifiable rewards, n.: Training an AI by letting it attempt problems whose answers can be checked automatically — a math result, a passing program — and rewarding it only when the check succeeds.
Sources
- de Moura, L., Kong, S., Avigad, J., van Doorn, F. & von Raumer, J. (2015). The Lean Theorem Prover (System Description). CADE-25, LNCS 9195.
- de Moura, L. & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language (System Description). CADE-28, LNCS 12699.
Mentioned in
automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement., formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way., interactive theorem provinginteractive theorem proving, n.: Writing a proof in a precise computer language so that software checks every step: the person supplies the ideas, the computer fills in small steps and guarantees that nothing is wrong., International Mathematical OlympiadInternational Mathematical Olympiad, prop. n.: The world's top math competition for high-school students. Because its problems demand creative written proofs, not just answers, earning a gold medal there became a famous test of AI reasoning, first passed in 2025., autoformalizationautoformalization, n.: Using AI to translate ordinary mathematics written for people — definitions, theorem statements, proofs — into a strict formal language that a proof-checking program can verify., IsabelleIsabelle, prop. n.: A widely used proof-checking program in which people write mathematics and verified software; it is known for automation that calls other theorem provers to finish routine steps., MathlibMathlib, prop. n.: A huge shared library of mathematics written in the Lean language, in which every definition and proof has been checked by computer. Mathematicians keep extending it, and AI proof systems are trained on it., miniF2FminiF2F, prop. n.: A test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics., RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step., satisfiability modulo theoriessatisfiability modulo theories, n.: An extension of logic-puzzle solving that also understands arithmetic, arrays and other data types, so it can check whether conditions in software, such as 'x + y > 10 and x < 3', can ever be met.