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	Lake Build System
5	Basics	Basics.lean
6	Data Structures	DataStructures.lean, MagicTheGathering.lean
7	Control Flow and Structures	ControlFlow.lean, FizzBuzz.lean, Collatz.lean, DndCharacter.lean
8	Polymorphism and Type Classes	Polymorphism.lean, SpellEffects.lean, Units.lean
9	Effects	Effects.lean, Transporter.lean
10	IO and Concurrency	IO.lean, WordFreq.lean
11	Proofs	Proving.lean
12	Type Theory	TypeTheory.lean
13	Dependent Types	TypeTheory.lean, DependentTypes.lean, VendingMachine.lean, NQueens.lean
14	Proof Strategy	ProofStrategy.lean
15	Tactics Reference	Tactics.lean
16	Congruence and Subtyping	Subtyping.lean
17	Classic Proofs	Proofs/
18	Algebraic Structures	AlgebraicStructures.lean
19	Mathlib	Mathlib.lean
20	Software Verification	Verification.lean, Compiler.lean, GameOfLife.lean, StackMachine.lean, ParserCombinators.lean
21	Artificial Intelligence	Auction.lean, Vickrey.lean, CombinatorialAuction.lean
22	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.