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.
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)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.
Theorem Proving
Explore dependent type theory and tactics. Learn to write proofs, understand Propositions as Types, and use Mathlib.
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.
Quick Start
Get up and running in under 5 minutes.
Install Lean
Install the elan toolchain manager:
1curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | shCreate a Project
Initialize a new Lean project:
1lake init my-project2cd my-project3lake buildStart Coding
Open in VS Code & install the Lean extension:
1-- Main.lean2def main : IO Unit :=3 IO.println "Hello!"As a Programming Language
Define data structures, write functions with pattern matching, and leverage Lean's powerful type inference.
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 mathematical theorems interactively. Use tactics to construct proofs step by step with compiler guidance.
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 [List.cons_append]9 exact ihJoin the Community
Lean has an active, welcoming community of researchers, educators, and developers.
Frequently Asked Questions
What is Lean 4?+
Lean 4 is a modern, open-source programming language and interactive theorem prover developed at Microsoft Research. It combines dependent type theory with a practical functional programming language, allowing you to write provably correct software and prove mathematical theorems.
Is Lean 4 free to use?+
Yes! Lean 4 is completely free and open-source under the Apache 2.0 license. You can use it for commercial or academic projects without any restrictions.
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 efficient C code for production use.
Do I need a math background to learn Lean 4?+
No! Our Language Guide teaches Lean as a programming language — no proofs required. If you're interested in theorem proving, you can explore that separately through our Tactics reference.
How long does it take to learn Lean 4?+
You can write basic Lean programs within a few hours using our guides. The fundamentals of the language take about 1-2 weeks. Theorem proving is a deeper topic that builds over time, but our guided lessons make it approachable for beginners.
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 (Mathlib4) is the community-maintained mathematical library for Lean 4 containing thousands of formalized theorems, tactics like ring, linarith, and omega, and data structures. It is the largest library 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 in VS Code for the best development experience with the interactive Infoview panel.
Ready to Begin?
Start with the programming guide or dive into theorem proving.