Introduction
Welcome to From Zero to QED, an informal introduction to formality in Lean 4. This article series teaches the language from first principles. Lean is expressive but the learning resources remain scattered and incomplete. This series is a best effort to fill that gap.
Note
This is the beta release. There are bound to be typos, errors, and rough edges. If you spot something, send a PR on GitHub.
Tip
Most Lean examples are included directly from source files checked by the main build, including deliberately rejected examples checked with
#guard_msgs. Standalone snippets and schematic blocks are not covered by that mechanism; the SMT examples are also outside the main build. Some teaching examples deliberately usesorry, which Lean accepts with a warning. The include checker validates source references, not every code block or every claim in the prose. The full source lives in the GitHub repository.
What This Series Covers
The series divides into two arcs. The first arc treats Lean as a programming language. You will learn the syntax, type system, control flow, polymorphism, monads, and IO. By the end of this arc you can write real programs in Lean.
The second arc treats Lean as a theorem prover. You will learn to write proofs, understand type theory and dependent types, master tactics, and eventually prove classic mathematical results. The series concludes with the emerging intersection of theorem proving with artificial intelligence, and why formal methods may matter more in the coming decade than they have in the previous five.
No prior experience with theorem provers is assumed. Familiarity with a typed functional language like Haskell, OCaml, or Scala helps but is not strictly required.
Getting Started
Follow the official Lean installation instructions.
Reading Paths
Different readers come to this material with different goals. Here are suggested paths through the series:
Complete beginners to typed functional programming: Read linearly. Arc I builds the programming foundation you need. Do not skip ahead to proofs until you are comfortable with pattern matching, recursion, and type classes. The concepts in Polymorphism are essential for understanding how Lean’s type system works.
Systems programmers wanting verification: Read Arc I thoroughly since you will use these features in production code. In Arc II, focus on Proofs, Proof Strategy, Verified Programs, and State Machine Verification. The Type Theory article provides the foundation but can be revisited as needed.
AI researchers interested in theorem proving: After covering the basics, jump to Proofs, then Tactics Reference, and finally Artificial Intelligence. The intermediate articles on type theory and algebraic structures can wait until you need them for specific formalization tasks.
Mathematicians new to programming: Start with Basics and Control Flow to learn Lean as a language, then proceed linearly through Arc II. You may skim Effects and IO on first reading since they focus on computational side effects rather than proof.
Article dependencies: Most articles build on previous ones, but some can be read independently. Classic Proofs requires Proofs, Proof Strategy including its section on termination proofs, and the workflow half of Mathlib, since every proof there leans on library lemmas. Algebraic Structures requires Type Classes. Mathlib requires familiarity with tactics from Proofs but not deep type theory.
Repository Structure
Code samples are extracted from Lean source files under src/. The book targets the Lean release pinned in the repository’s lean-toolchain file (Lean 4.34 at the time of writing) with the matching Mathlib; when the prose describes a feature, it is one that release has. Each chapter corresponds to one or more modules, and lake build compiles all of them:
Runnable examples live in src/Examples/ and are exercised by CI:
| Example | Source File | Run Command |
|---|---|---|
| FizzBuzz | FizzBuzz.lean | lake exe fizzbuzz 20 |
| Collatz | Collatz.lean | lake exe collatz 27 |
| Word Frequency | WordFreq.lean | lake exe wordfreq "the spice must flow" |
| D&D Character Generator | DndCharacter.lean | lake exe dnd 42 |
| Units of Measure | Units.lean | lake exe units |
| Magic: The Gathering | MagicTheGathering.lean | lake exe mtg |
| Spell Effects | SpellEffects.lean | lake exe spells |
| ATM Withdrawal | ATM.lean | lake exe atm |
| Vending Machine | VendingMachine.lean | lake exe vending |
| N-Queens | NQueens.lean | lake exe nqueens |
| Parser Combinators | ParserCombinators.lean | lake exe parsers |
| Stack Machine | StackMachine.lean | lake exe stack |
| Game of Life | GameOfLife.lean | lake exe life |
| Circuit Breaker | CircuitBreaker.lean | cargo test -p circuit-breaker |
Open these files in VS Code to explore with full IDE support. The Infoview panel shows types and proof states as you navigate.
Additional learning resources are collected in the References appendix. This series is an informal introduction to formality. If you want the stuffy formal introduction to formality, see Theorem Proving in Lean 4, Functional Programming in Lean, Mathematics in Lean, or university courses from CMU, Imperial, and Brown. They are more rigorous.