Lean

Overview

Lean is a functional programming language and interactive theorem prover (proof assistant) built on dependent type theory. It is unusual in being simultaneously a serious general-purpose programming language and a system in which mathematical statements can be stated precisely and their proofs checked mechanically by a small, trustworthy kernel. In Lean, a program and a proof are written in the same language and verified by the same type checker — a consequence of the Curry–Howard correspondence, under which propositions are types and proofs are programs.

Lean was created by Leonardo de Moura and first appeared in 2013. Since then it has gone through several major redesigns, culminating in Lean 4, a self-hosted reimplementation that compiles to efficient C code and is fast enough to be used for ordinary software, not just proofs.

History and Origins

The Lean project was launched in 2013 by Leonardo de Moura, a Brazilian computer scientist, while he was at Microsoft Research in Redmond. De Moura was already well known in formal methods as a principal author of the Z3 SMT solver, and Lean grew out of a desire for a flexible, open, and highly extensible theorem prover that could serve both as a research vehicle and as a practical tool.

The first public release, Lean 0.1, arrived around 2014. The early Lean 1 and Lean 2 versions were experimental and explored ideas — including support for homotopy type theory — that were later dropped as the design matured. Lean 3, released in January 2017, was the first reasonably stable and widely adopted version. It was implemented largely in C++, with a powerful metaprogramming and tactic framework written in Lean itself, which made it attractive to mathematicians and led to the founding of the community mathematics library mathlib the same year.

In 2021, de Moura and collaborators released Lean 4, a ground-up rewrite. Lean 4 is largely self-hosted — much of the compiler and elaborator is written in Lean — and it can produce compiled C code, turning Lean into a credible general-purpose programming language as well as a proof assistant. The first official stable Lean 4 release, 4.0, appeared in September 2023.

In July 2023, the Lean Focused Research Organization (Lean FRO) was founded by Leonardo de Moura and Sebastian Ullrich under Convergent Research, a nonprofit dedicated to a focused five-year mission of improving Lean’s scalability, usability, documentation, and proof automation, and guiding the project toward long-term sustainability independent of any single corporate sponsor.

Design Philosophy

Lean is shaped by a few central commitments:

• One language for programs and proofs. Because Lean is based on a dependently typed lambda calculus, the same constructs express computations and mathematical arguments. A theorem is a type; a proof is a term of that type; the type checker is the proof checker.
• A small trusted kernel. Proofs are ultimately reduced to terms that a compact, carefully scrutinized kernel verifies. Everything else — tactics, automation, elaboration — only has to produce something the kernel will accept, so bugs in higher layers cannot make a false statement appear proven.
• Extensibility through metaprogramming. Lean exposes its own internals so that users can write tactics, custom syntax, and notation in Lean itself. Lean 4 takes this further, letting users extend the language’s parser and elaborator, effectively building domain-specific languages on top of Lean.
• Performance as a first-class concern. Lean 4’s compilation to C and its efficient runtime were deliberate goals, intended to make Lean usable for real software and to keep large proof developments responsive.

Key Features

• Dependent type theory. Lean is based on a version of the Calculus of Constructions extended with inductive types, allowing types to depend on values and enabling extremely expressive specifications.
• Interactive tactic proofs. Users build proofs interactively using tactics (such as intro, apply, rw, simp, and induction), with the editor showing the evolving proof goal at each step.
• Term-mode proofs. Proofs can also be written directly as terms, blurring the line between writing a program and writing a proof.
• Powerful metaprogramming. New tactics, notation, and even syntax extensions can be defined in Lean itself.
• Compilation to C. Lean 4 programs compile to C and then to native code, with a runtime that uses reference counting and other techniques for efficiency.
• Strong tooling. First-class editor integration (notably VS Code, plus Neovim and Emacs), the Lake build system, and the elan toolchain manager support real-world development.
• mathlib ecosystem. A continually growing, community-maintained library of formalized mathematics provides reusable definitions and theorems across many fields.

Lean is distributed as free, open-source software under the Apache License 2.0. According to its documentation, Lean runs on Linux, macOS, and Windows on common 64-bit architectures.

Evolution

Lean’s history is a story of repeated, deliberate reinvention. The experimental Lean 1 and 2 releases established the core idea; Lean 3 turned it into a practical proof assistant and attracted the mathematics community that built mathlib; and Lean 4 rebuilt the system to be self-hosting, extensible, and fast enough to double as a programming language. Each transition required substantial migration effort — porting mathlib from Lean 3 to Lean 4 was itself a large community undertaking — but the result has been a system that few of its contemporaries can match in combining mathematical expressiveness with software-engineering practicality.

The formation of the Lean FRO in 2023 marked another important shift: from a project driven largely by one researcher and a volunteer community to a dedicated organization with stable funding and a clear roadmap.

Current Relevance

Lean occupies a prominent position in the modern formal-methods landscape. Among working mathematicians it has become arguably the most visible proof assistant, propelled by high-profile formalizations such as the Liquid Tensor Experiment (verifying a theorem from Peter Scholze’s condensed mathematics) and Terence Tao’s rapid formalization of the polynomial Freiman-Ruzsa conjecture. These efforts demonstrated that Lean can keep up with research-level mathematics and that formalization can be a practical part of doing new mathematics, not merely an after-the-fact curiosity.

Lean is also central to a wave of research on AI-assisted theorem proving. Because its proofs are precise and machine-checkable, Lean serves as an ideal training and evaluation environment for machine-learning systems that attempt to generate formal proofs — a setting where an automated prover’s output can be verified beyond doubt rather than merely judged plausible. Beyond mathematics, Lean’s status as a dependently typed general-purpose language makes it a candidate for software and hardware verification.

Why It Matters

Lean matters because it brings the once-arcane idea of fully formal, machine-checked proof close to mainstream mathematical and computational practice. By unifying programming and proving in one expressive, performant, open system — and by pairing it with mathlib, one of the largest formal libraries ever assembled — Lean has made formalization fast enough and pleasant enough that leading mathematicians use it on current research. It stands as a leading example of dependent type theory escaping the lab and becoming a tool that ordinary practitioners, and increasingly AI systems, can wield to establish results with absolute certainty.