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	Termination and Well-Founded Recursion	Termination.lean
9	Standard Library and Batteries	StdLibrary.lean
10	Polymorphism and Type Classes	Polymorphism.lean, SpellEffects.lean, Units.lean
11	Effects	Effects.lean, ATM.lean
12	IO and Concurrency	IO.lean, WordFreq.lean
13	Proofs	Proving.lean
14	Type Theory	TypeTheory.lean
15	Dependent Types	TypeTheory.lean, DependentTypes.lean, VendingMachine.lean, NQueens.lean
16	Proof Strategy	ProofStrategy.lean
17	Congruence and Subtyping	Subtyping.lean
18	Classic Proofs	Proofs/
19	Algebraic Structures	AlgebraicStructures.lean
20	Mathlib	Mathlib.lean
21	Verified Programs	Verification.lean, Compiler.lean, GameOfLife.lean, StackMachine.lean, CircuitBreaker.lean, ParserCombinators.lean
22	Model Checking	ModelChecking.lean
23	Artificial Intelligence	Auction.lean, Vickrey.lean, CombinatorialAuction.lean
24	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.