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
This article is itself a giant checkable theorem. Every code sample, every proof, every definition is extracted from source files that the Lean compiler typechecks on every build. If the article compiles, the theorems are valid. 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 Model Checking. 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 only Proofs and Proof Strategy. Algebraic Structures requires Type Classes. Mathlib requires familiarity with tactics from earlier articles but not deep type theory.
Repository Structure
Code samples are extracted from Lean source files. Each article corresponds to modules in the src/ directory:
| Article | Source File |
|---|---|
| Basics | src/ZeroToQED/Basics.lean |
| Data Structures | src/ZeroToQED/DataStructures.lean |
| Control Flow | src/ZeroToQED/ControlFlow.lean |
| Polymorphism | src/ZeroToQED/Polymorphism.lean |
| Effects | src/ZeroToQED/Effects.lean |
| IO | src/ZeroToQED/IO.lean |
| Proofs | src/ZeroToQED/Proving.lean |
| Type Theory | src/ZeroToQED/TypeTheory.lean |
| Tactics | src/ZeroToQED/Tactics.lean |
Larger examples live in src/Examples/:
| Example | Source File | Run Command |
|---|---|---|
| Magic: The Gathering | MagicTheGathering.lean | lake exe mtg |
| D&D Character Generator | DndCharacter.lean | lake exe dnd 42 |
| ATM Withdrawal | ATM.lean | lake exe atm |
| Parser Combinators | ParserCombinators.lean | lake exe parsers |
| Game of Life | GameOfLife.lean | lake exe life |
| Stack Machine | StackMachine.lean | lake exe stack |
| 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.