Lean

Lean is a modern theorem prover and dependently typed programming language developed primarily by Leonardo de Moura at Microsoft Research. First released in 2013, with the current major version Lean 4 appearing in 2021, Lean represents a convergence of automated reasoning, interactive theorem proving, and general-purpose programming. It is built on a variant of the Calculus of Inductive Constructions similar to Coq, but with a stronger emphasis on automation, performance, and usability. Lean is the proof assistant of choice for the mathlib project, one of the largest unified libraries of formalized mathematics in existence.

Unlike older proof assistants that were designed primarily for verification, Lean is designed as a programming language first and a theorem prover second. It features a native code compiler, a metaprogramming framework, and a library system that feels closer to modern software development than to traditional formal methods. This design choice has attracted a large community of mathematicians and computer scientists who use Lean for both research and teaching.

Lean 4 and the Metaprogramming Revolution

Lean 4 is a complete reimplementation that compiles to C and then to native machine code. It is fast enough to write proof tactics, parser extensions, and even domain-specific compilers within Lean itself. The metaprogramming framework allows users to write custom tactics, elaborators, and syntactic extensions in Lean, using the same language for proofs and proof automation. This eliminates the traditional barrier between the object language (the language being reasoned about) and the meta-language (the language writing the reasoner). In Lean, they are the same.

The tactic system in Lean 4 is based on tactic monads, which provide a structured way to manipulate proof goals, handle errors, and backtrack. Lean's automation includes simp (a powerful simplifier with conditional rewriting), linarith (linear arithmetic reasoning), ring (algebraic normalization), and aesop (a general-purpose proof search tactic). These tactics are implemented as Lean programs, making them extensible and inspectable.

mathlib and the Formalization of Mathematics

The mathlib project is the largest library of formalized mathematics, covering algebra, analysis, topology, number theory, combinatorics, and more. It is developed by a distributed community of hundreds of contributors, using continuous integration and code review practices borrowed from software engineering. Mathlib is not merely a collection of isolated proofs; it is a unified, interconnected body of mathematics where results from one domain can be applied to another without friction.

The scale of mathlib is significant: it contains over a million lines of formalized mathematics, covering substantial portions of undergraduate and graduate-level mathematics. The project has demonstrated that large-scale collaborative mathematics is possible in a formal setting, and it has become a model for how formalized mathematics can be organized and maintained.

Lean in Verification and Industry

While Lean is best known for mathematics, it is also used in software verification. The LeanAide project and other tools explore the use of Lean for proving properties of programs. The language's dependent types allow specifications to be embedded directly in types, making incorrect programs unrepresentable. Lean's native code generation means that verified programs can be extracted to efficient executable code.

The Lean community has also developed tools for teaching, including the Natural Number Game and Theorem Proving in Lean, which introduce formal proof through interactive puzzles. These educational tools have lowered the barrier to entry for formal methods, attracting students and researchers who might not otherwise engage with proof assistants.

Lean is the proof assistant that learned from the mistakes of its predecessors. Where Coq is austere and Isabelle is classical, Lean is pragmatic. It does not ask users to choose between constructivity and classicality, between automation and control, between mathematics and programming. It provides all of them, and in doing so it has built the largest community of practicing formalizers in history. The question is not whether Lean will dominate theorem proving. The question is whether theorem proving, through Lean, will finally become a normal part of how mathematics and software are done. The mathlib project suggests the answer is yes — and the implication is that every field of knowledge will eventually have its own mathlib, a formalized, checkable, and extensible foundation.