Lean is an open-source proof assistant and programming language for expressing mathematical definitions, constructing proofs, and verifying that proofs satisfy precise logical rules. It supports the formalization of mathematics and the formal verification of software. Its defining architectural distinction is between sophisticated tools that help construct proofs and a comparatively small kernel that checks the resulting proof terms. Lean 4 also serves as a general-purpose functional programming language, allowing users to implement programs and proof automation within the same environment. (lean-lang.org)
Origins and development
Leonardo de Moura launched the Lean project at Microsoft Research in 2013. Lean 0.1 was officially released on June 16, 2014. The project sought to combine the assurance provided by a small, independently implementable proof checker with the convenience of automated reasoning tools. This combination allows substantial automation without requiring every proof-construction procedure to belong to the trusted logical core. (lean-lang.org)
Lean 4 is a substantial reimplementation rather than merely an incremental extension of earlier versions. Its system-description paper, published in 2021 by de Moura and Sebastian Ullrich, describes an extensible frontend and an implementation largely written in Lean itself. Features include user-defined syntax, macros, elaboration procedures, and tactics. The mathematical community subsequently migrated its library from Lean 3 to Lean 4, using a porting tool called mathport; the two generations are not interchangeable at the source-code level. (lean-lang.org)
Logical foundations
Lean’s foundation is dependent type theory, in which a type may depend on a value. This permits expressions such as a type of vectors indexed by their length, alongside ordinary function and data types. Its core theory includes dependent functions, inductive types, a hierarchy of universes, and a distinguished type Prop for propositions. Universes organize types into levels rather than treating every type as an element of one unrestricted type of all types. (lean-lang.org)
The relationship between propositions and proofs follows the Curry–Howard correspondence: a proposition is represented as a type, and a proof is a term inhabiting that type. For example, a proof of an implication P → Q is a function that transforms evidence for P into evidence for Q. Checking a formal proof therefore amounts to checking that its proof term has the type corresponding to the claimed theorem. (lean-lang.org)
Inductive definitions describe objects such as natural numbers and lists through constructors and associated elimination principles. These support definitions by recursion and proofs by mathematical induction. Lean also supports classical reasoning through additional principles, including choice, propositional extensionality, and quotient soundness. Their use is tracked as an axiomatic dependency rather than being concealed within proof syntax. (docs.lean-lang.org)
Proof construction and checking
Users can write proof terms directly or construct them interactively with tactics. A tactic is a program that transforms a proof state, consisting of outstanding goals and available assumptions. Common operations introduce hypotheses, apply existing theorems, rewrite expressions using equalities, or simplify a goal. Tactic scripts ultimately construct proof terms; they are not themselves additional logical inference rules. (lean-lang.org)
For example, the following Lean 4 declaration proves that a proposition implies itself:
theorem identity_implication (P : Prop) : P → P := by
intro h
exact h
Here, intro h introduces the assumed proof of P, and exact h supplies that proof as the conclusion. The corresponding direct proof term is fun h => h. More elaborate proofs can combine explicit intermediate statements with automation such as simp, which performs theorem-based simplification. (lean-lang.org)
Before checking, elaboration translates convenient surface syntax into explicit core expressions. It resolves omitted arguments, overloaded notation, coercions, and other information inferred from context. The kernel then checks declarations independently of those inference procedures. This separation limits the consequences of frontend or tactic bugs: an incorrectly constructed ordinary proof term should be rejected by the kernel. (lean-lang.org)
Programming and mathematical libraries
Lean 4 combines functional programming with facilities for practical executable software. Its extensibility lets users write metaprograms that manipulate expressions and implement specialized automation. Type classes organize reusable interfaces and support automatic instance selection, including the algebraic structures needed to interpret mathematical notation. Lake, Lean’s build and package-management tool, organizes projects, dependencies, libraries, and executables. (lean-lang.org)
The principal community mathematical library is Mathlib. It contains definitions, theorems, programming infrastructure, and tactics, with coverage spanning algebra, linear algebra, topology, analysis, and measure theory. Its shared hierarchy of structures allows results to be stated under reusable assumptions instead of redeveloping each mathematical subject independently. Contributions follow community conventions for naming, style, documentation, and review. (github.com)
Scope and trust boundaries
Lean checks the formal statement actually encoded, not whether that statement faithfully captures an author’s informal intention. Accordingly, a checked proof establishes derivability within its definitions and assumptions; interpreting those definitions remains a separate task. This distinction matters in both mathematical formalization and verification of software specifications. (leanprover-community.github.io)
Successful processing of a file is also not sufficient evidence that every theorem has a completed proof. The placeholder sorry uses sorryAx, which can inhabit arbitrary types. Lean’s #print axioms command exposes direct and indirect axiom dependencies. Proofs relying on native evaluation additionally depend on compiled computation, enlarging the trust boundary beyond ordinary kernel checking. These distinctions separate completed kernel-checked proofs from unfinished declarations or results dependent on additional assumptions. (lean-lang.org)