Fermat’s Last Theorem, checked line by line
A 350-year story meets an 11-day formalization campaign.
Read the story →Interactive Lean 4 Academy
Learn Lean 4 by writing code and proofs.
Start in your browser, run Lean, and build a proof one checked step at a time.
Follow 130 lessons from core types and functions to induction, verified programs, and proof terms. The reference guides remain available whenever you need the details.
lean|welcome.lean
1-- Welcome to Lean 42def hello : String := "Hello, Lean!"34-- A simple theorem5theorem add_comm (a b : Nat) : a + b = b + a := by6 omega78-- Functional programming with pattern matching9def fibonacci : Nat → Nat10 | 0 => 011 | 1 => 112 | n + 2 => fibonacci n + fibonacci (n + 1)13
Courses
130
Lessons
38
Free lessons
Lean4 Academy
Start with the language. End with verified programs.
Each lesson introduces one idea, shows it in Lean, and gives you an exercise to finish in the browser.
- 01Start hereLean as a language, the first proof tactics, and propositional logic.Free
- 02Proof techniquesQuantifiers, rewriting, simp, omega and calc, and proofs written as terms.Pass
- 03Programs and inductionRecursive programs, induction on numbers, lists and trees, and specifications you prove.Pass
- 04Natural Number LabArithmetic built from zero and successor, through order and divisibility.Pass
- 05Advanced proofs and effectsProof-carrying data, length-indexed vectors, monads and their laws.Pass
Lean4 Problems
Practise on problems the compiler judges.
45 programming and proof problems. Programs run against hidden tests; proofs are accepted only when Lean closes every goal. Easy problems and the daily problem are free, with a leaderboard and streaks for regular practice.
- 01Fizz BuzzDescribe a number the way the counting game does.Program
- 02Swap a conjunctionFrom P and Q, conclude Q and P.Proof
- 03PalindromeDecide whether a string reads the same in both directions.Program
- 05ContrapositiveIf P implies Q, then not Q implies not P.Proof
- 06Climbing stairsCount the ways up a staircase, fast enough for fifty steps.Program
Mathematics, in progress
Behind the proof
The Jacobian conjecture meets a counterexample
A local-to-global intuition overturned by three polynomials.
Read the story →Navier–Stokes: a new proof claim, and a dispute over credit
A fluid singularity, a Lean certificate, and two accounts of the race.
Read the story →Follow the original sources, inspect the Lean work, and discuss it with the community.
Coursework and reference, in one place.
Follow the Academy in order, or use the language and tactics pages when you need one specific answer.
Interactive Academy
13 courses with exercises checked by Lean and progress saved to your account.
10-course curriculum
Functional Programming
Lean as a programming language: syntax, types, data structures, monads, and projects built with Lake.
Language Guide
Theorem Proving
Writing proofs with tactics: propositions as types, the core tactics, automation, and Mathlib.
Tactics Reference
Why Lean 4?
Pure Functional Design
Immutable data, pattern matching and higher-order functions, checked by a strict type system.
Dependent Types
Types can depend on values, so an invariant such as the length of a list can be part of a function's type.
Interactive Proving
Proofs are written one tactic at a time, and the editor shows the goals that remain after each step.
Compiled to Native Code
Lean compiles to C and then to native executables. Lake builds projects and manages dependencies.
Quick Start
Install Lean, create a project, and open it in your editor.
1
Install Lean
Install the elan toolchain manager:
bash
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh2
Create a Project
Initialize a new Lean project:
bash
lake init my-projectcd my-projectlake build3
Start Coding
Open in VS Code & install the Lean extension:
lean
-- Main.leandef main : IO Unit := IO.println "Hello!"As a Programming Language
Define data structures and write functions with pattern matching. Lean infers most of the types.
lean
1structure Person where2 name : String3 age : Nat4 deriving Repr56def greet (p : Person) : String :=7 s!"Hello, {p.name}!"89def adults (people : List Person) : List Person :=10 people.filter (·.age ≥ 18)1112#eval greet { name := "Alice", age := 30 }As a Theorem Prover
Prove theorems one tactic at a time. After each step, Lean shows what is left to prove.
lean
1-- Prove that list append is associative2theorem append_assoc {α : Type} 3 (xs ys zs : List α) :4 xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := by5 induction xs with6 | nil => simp7 | cons x xs ih =>8 simp only [List.cons_append, ih]Join the Community
Mathematicians, computer scientists and programmers use Lean, and many of them answer questions in public forums.
Frequently Asked Questions
What is Lean 4?+
Lean 4 is an open-source programming language and interactive theorem prover. It began at Microsoft Research and is now developed by the Lean FRO together with a large community. You use the same language to write programs, to state facts about them, and to prove theorems in mathematics.
Is Lean 4 free to use?+
Yes. Lean 4 is open source under the Apache 2.0 license, which allows both commercial and academic use. If you redistribute Lean itself, the license asks you to keep its notices.
What can I build with Lean 4?+
You can use Lean 4 for general-purpose functional programming (building CLI tools, libraries, and applications), formal verification (proving software correctness), and mathematical theorem proving (formalizing proofs for research or education). Lean compiles to C and from there to native executables.
Do I need a math background to learn Lean 4?+
No. The Academy starts with programming foundations, teaches you to read a proof goal, and builds one step at a time. The first three courses are free.
How long does it take to learn Lean 4?+
Simple programs take a few hours to write. The core of the language takes a week or two. Theorem proving takes longer; the free Academy courses start from the beginning and assume no background.
What is do notation in Lean 4?+
Do notation in Lean 4 is syntactic sugar for sequencing monadic computations. It desugars to bind (>>=) calls, letting you write imperative-style code with let, mut, for-in loops, and early returns that translate to pure functional operations under the hood.
What is Lake in Lean 4?+
Lake is Lean 4's built-in build system and package manager. You use it to create projects (lake init), manage dependencies (lake add), and build executables (lake build). It's configured via a lakefile.lean file in your project root.
What is Mathlib?+
Mathlib is the community-maintained mathematics library for Lean 4. It covers algebra, analysis, topology, number theory and more, and adds tactics such as ring and linarith. It is one of the largest libraries of formalized mathematics in any proof assistant.
How do I install Lean 4?+
Install Lean 4 using elan, the Lean version manager. On macOS/Linux run: curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh. Then install the Lean 4 extension for VS Code, which shows goals and errors in the Infoview panel as you type.
Write your first checked Lean proof.
Begin with 38 free lessons. Upgrade only when you are ready for the full curriculum.