Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

Lean 4 is an open-source, statically typed functional programming language and interactive theorem prover developed at Microsoft Research and now maintained by the Lean FRO. It unifies the worlds of software engineering and formal mathematics: the same language you use to write executable programs is the language you use to state and prove theorems about those programs. By reading this page you will understand what makes Lean 4 unique, its key features, and where to go next.

​
What is Lean 4?

Lean 4 is built on a small, well-understood kernel of dependent type theory called the Calculus of Constructions. Every expression has a type, and types themselves are first-class values. This means you can write a function whose return type depends on the value of its argument — so a list’s length can be part of the list’s type — and the compiler will enforce those invariants at compile time. Lean 4 is also a metaprogramming platform: its tactic framework, macro system, and elaborator are all written in Lean itself, making the language highly extensible. 
-- The classic first program
def main : IO Unit :=
  IO.println "Hello, Lean 4!"

Dependent Types

Express rich invariants in the type system. Values can appear inside types, enabling precise specifications such as Vector α n — a list of exactly n elements.

Tactic Proofs

Prove theorems interactively using a powerful tactic language. Tactics like simp, omega, decide, rfl, and induction automate most routine steps.

Metaprogramming

Extend Lean itself. Macros, custom tactics, and elaboration extensions are written in Lean and run at compile time, giving you a full macro system and DSL toolkit.

Lake Build System

Lake is Lean 4’s integrated build system and package manager. It handles dependencies, compilation, and running executables with a lakefile.toml (or lakefile.lean) configuration.

Language Server (LSP)

First-class editor support via the Language Server Protocol. VS Code, Emacs, and Neovim all offer real-time error reporting, go-to-definition, and goal state displays.

FFI & C Interop

Call into C libraries directly with @[extern] declarations. Lean manages its own memory with a reference-counting GC that integrates cleanly with C.

​
Lean 4 as a Programming Language

Lean 4 is a pure functional language with a strict (call-by-value) evaluation strategy. It supports the features you expect from a modern functional language:
  • Algebraic data types defined with inductive
  • Pattern matching with match
  • Type classes for ad-hoc polymorphism (Add, Monad, Repr, …)
  • Monadic do-notation for IO, state, exceptions, and more
  • Efficient compilation to native code via LLVM or to C
-- Algebraic data type
inductive Shape where
  | circle    (radius : Float) : Shape
  | rectangle (width height : Float) : Shape

-- Pattern matching
def area : Shape → Float
  | .circle r    => 3.14159265358979 * r * r
  | .rectangle w h => w * h

#eval area (.circle 3.0)        -- 28.274333...
#eval area (.rectangle 4.0 5.0) -- 20.0

​
Lean 4 as a Theorem Prover

A proposition in Lean is just a type in Prop. A proof of that proposition is a term that inhabits the type. This is the Curry–Howard correspondence: programs and proofs are the same thing, and the type checker verifies both. 
-- A simple theorem about natural numbers
theorem add_comm_zero (n : Nat) : n + 0 = n := by
  simp

-- Structural induction
theorem add_assoc' (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction c with
  | zero      => simp
  | succ c ih => simp [Nat.add_succ, ih]
Lean’s kernel is a small, independently verifiable trust anchor. All proofs are checked by the kernel regardless of which tactics were used to build them.

​
Brief History

VersionMilestone
Lean 1–3Developed 2013–2019 at Microsoft Research by Leonardo de Moura. Established Lean as a serious ITP.
Lean 4Complete rewrite announced 2018, stable release 2023. The compiler, tactics, and standard library are all written in Lean itself.
Lean FROThe Lean Focused Research Organization (non-profit) was founded in 2023 to support long-term development.

​
Community and Resources

Official Website

Homepage with news, examples, and the documentation overview.

Theorem Proving in Lean 4

The definitive free book for learning Lean as a proof assistant.

Functional Programming in Lean

A free book teaching Lean 4 as a functional programming language.

Zulip Chat

The main community hub for questions, announcements, and discussion.
If you are new to Lean 4, the fastest path is: install elan → run lake new hello → open the folder in VS Code with the Lean 4 extension. See the Quickstart for step-by-step instructions.

Build docs developers (and LLMs) love

Get started for freeTalk to us