From Zero to QED

An informal introduction to formality in Lean 4.

Read

• HTML - Read online
• PDF - Download for offline reading

Try Online

No local setup required. Launch a complete Lean 4 environment in your browser:

• Open in GitHub Codespaces - Free for 120 core-hours/month
• Open in Gitpod - Free tier available

The environment comes pre-configured with Lean 4, the VS Code extension, and all dependencies.

Try Locally

Install Lean 4 with VS Code and the Lean 4 extension, then:

git clone https://github.com/sdiehl/zero-to-qed
cd zero-to-qed
lake exe cache get   # Download prebuilt Mathlib
lake build

Alternatively, if you have Docker and VS Code installed, clone the repo and open it in VS Code. You'll be prompted to "Reopen in Container" which builds the same environment on your machine.

Contents

#	Prose	Code
1	Introduction
2	Why?
3	Theorem Provers
4	Basics	Basics.lean
5	Lake Build System
6	Data Structures	DataStructures.lean, MagicTheGathering.lean
7	Control Flow and Structures	ControlFlow.lean, FizzBuzz.lean, Collatz.lean, DndCharacter.lean
8	Standard Library and Batteries	StdLibrary.lean
9	Polymorphism and Type Classes	Polymorphism.lean, SpellEffects.lean, Units.lean
10	Effects	Effects.lean, ATM.lean
11	IO and Concurrency	IO.lean, WordFreq.lean
12	Proofs	Proving.lean
13	Type Theory	TypeTheory.lean
14	Dependent Types	TypeTheory.lean, DependentTypes.lean, VendingMachine.lean, NQueens.lean
15	Proof Strategy	ProofStrategy.lean
16	Congruence and Subtyping	Subtyping.lean
17	Classic Proofs	Proofs/
18	Algebraic Structures	AlgebraicStructures.lean
19	Mathlib	Mathlib.lean
20	Verified Programs	Verification.lean, Compiler.lean, GameOfLife.lean, StackMachine.lean, CircuitBreaker.lean, ParserCombinators.lean
21	Model Checking	ModelChecking.lean
22	Artificial Intelligence	Auction.lean, Vickrey.lean, CombinatorialAuction.lean
23	References

Contributing

See BUILD.md for details on the HTML and PDF build pipeline. Add yourself to CONTRIBUTORS.md and submit a PR.

License

Software (Lean code in src/): MIT License. See LICENSE.

Prose (text in docs/): Public domain. Share it, adapt it, translate it. I just ask that you not sell it. It is meant to be free.