Robots Atlas>ROBOTS ATLAS
Reasoning

Lean 4

2013ActivePublished: 16 October 2026Updated: 16 October 2026Published
Key innovation
Unifies a dependent type system (the Calculus of Inductive Constructions) with a fast functional programming language, so that mathematical proofs and verified code are written in one environment, and the proof assistant itself is fully extensible from within Lean.
Category
Reasoning
Abstraction level
System
Operation level
InferenceAgent runtime
Use cases
Mathematics formalizationSoftware and hardware verificationAI automated theorem provingInteractive theorem provingTeaching formal logic and mathematicsFunctional programming

How it works

The user writes definitions and theorems in a dependently typed language where a theorem is a type and its proof is a term of that type (the Curry-Howard correspondence). Proofs are built interactively with tactics (e.g. simp, grind, induction) that transform a proof goal until it is closed. An elaborator expands notation, infers types and resolves type-class instances, and then a small trusted kernel re-checks the resulting proof term. Lean 4 compiles programs to C code, and its hygienic macro system lets users extend syntax and automation directly from within Lean.

Problem solved

Informal mathematical proofs and ordinary code can hide subtle errors that human review and testing miss. Lean lets a theorem or a program property be stated formally and machine-checked for completeness and correctness, reducing trust to a small, well-audited kernel.

Components

Trusted kernelSmall trusted kernel that re-checks every proof term; the only component that must be trusted for soundness.
ElaboratorExpands notation, infers types, resolves type-class instances and turns source into fully elaborated terms for the kernel.
Tactic frameworkExpressive tactic language (e.g. simp, grind, induction) for interactive and automated proof construction.
Hygienic macro systemHygienic macro system allowing syntax and automation to be extended directly in Lean.

Official

Implementation

Reference implementations
lean4
Lean, C++ · Lean FRO
Official
mathlib4
Lean · Lean community
Implementation pitfalls
Lean 4 is not backwards-compatible with Lean 3High

Lean 4 is not backwards-compatible with Lean 3; Lean 3 code and proofs must be ported (the mathport effort).

A proof is only as trustworthy as the kernelMedium

Verification relies on kernel soundness; in 2026 a purported disproof of the Collatz conjecture turned out to rely on a bug in Lean, which was subsequently fixed.

Evolution

Original paper · 2015 · CADE-25 2015 · Leonardo de Moura
The Lean Theorem Prover (System Description)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2013
Lean launched
Inflection point

Leonardo de Moura starts the project at Microsoft Research; early versions (Lean 1 and 2) were experimental.

2017
Lean 3

First moderately stable version (20 January 2017), implemented mainly in C++; the mathlib library grew around it.

2021
Lean 4
Inflection point

Reimplementation capable of producing C code; hygienic macro system and a frontend implemented in Lean itself. Not backwards-compatible with Lean 3.

2023
Lean FRO formed

The nonprofit Lean Focused Research Organization is formed to improve the language's scalability and usability.

2024
AlphaProof proves in Lean
Inflection point

Google DeepMind creates AlphaProof, proving mathematical statements in Lean at the level of an IMO silver medalist.

AI achieves silver-medal standard solving International Mathematical Olympiad problems (paper)
2025
DeepSeek-Prover-V2

DeepSeek introduces DeepSeek-Prover-V2, a theorem-proving model for Lean 4 built on DeepSeek-V3.

Hardware requirements

Primary

Lean 4 compiles to C code and runs cross-platform (Linux, macOS, Windows) on x86-64 and AArch64 CPUs; it needs no accelerators.