Learn Lean 4

A modern functional programming language and interactive theorem prover. Write provably correct software.

Master dependent type theory, build verified programs, and prove mathematical theorems with one of the most powerful type systems available.

Start Learning Documentation

lean|welcome.lean

1-- Welcome to Lean 4
2def hello : String := "Hello, Lean!"
3
4-- A simple theorem
5theorem add_comm (a b : Nat) : a + b = b + a := by
6  omega
7
8-- Functional programming with pattern matching
9def fibonacci : Nat → Nat
10  | 0 => 0
11  | 1 => 1
12  | n + 2 => fibonacci n + fibonacci (n + 1)

Two Perspectives, One Language

Lean 4 excels both as a general-purpose functional programming language and as a powerful theorem prover for formal mathematics.

Functional Programming

Learn Lean as a programming language. Syntax, types, data structures, monads, and building real applications with Lake.

Language Guide

Theorem Proving

Explore dependent type theory and tactics. Learn to write proofs, understand Propositions as Types, and use Mathlib.

Tactics Reference

Interactive Course

Learn by doing. Progress through guided exercises, from basic syntax to proving mathematical theorems interactively.

Start Course

Why Lean 4?

Pure Functional Design

Immutable data structures, pattern matching, and higher-order functions. Write clean, composable code with strong type guarantees.

Dependent Types

Types can depend on values, enabling you to encode invariants directly in your type signatures and prove properties at compile time.

Interactive Proving

A rich tactic language for step-by-step proof construction. The compiler guides you through proofs with precise error messages.

Real-World Ready

Compile to efficient native code. Lake build system for package management. Built for both research and production use.

As a Programming Language

Define data structures, write functions with pattern matching, and leverage Lean's powerful type inference.

lean

1structure Person where
2  name : String
3  age : Nat
4  deriving Repr
5
6def greet (p : Person) : String :=
7  s!"Hello, {p.name}!"
8
9def adults (people : List Person) : List Person :=
10  people.filter (·.age ≥ 18)
11
12#eval greet { name := "Alice", age := 30 }

As a Theorem Prover

Prove mathematical theorems interactively. Use tactics to construct proofs step by step with compiler guidance.

lean

1-- Prove that list append is associative
2theorem append_assoc {α : Type} 
3  (xs ys zs : List α) :
4  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by
5  induction xs with
6  | nil => simp
7  | cons x xs ih =>
8    simp [List.cons_append]
9    exact ih

Ready to Begin?

Start with the interactive course for a guided learning experience, or dive into the documentation if you prefer self-directed study.

Start the Course Read the Docs