From Zero to QED

An informal introduction to formality in Lean 4.

Read

Read Online: sdiehl.github.io/zero-to-qed

PDF: zero-to-qed.pdf (or print version for browser printing)

Contents

#	Prose	Code
1	Introduction
2	Why?
3	Theorem Provers
4	Build System
5	Basics	Basics.lean
6	Control Flow	ControlFlow.lean
7	Polymorphism	Polymorphism.lean
8	Effects	Monads.lean
9	IO and Concurrency	Effects.lean
10	Proofs	Proving.lean
11	Type Theory	TypeTheory.lean
12	Dependent Types	DependentTypes.lean
13	Proof Strategy	ProofStrategy.lean
14	Tactics	Tactics.lean
15	Subtyping	Subtyping.lean
16	Mathematics	Mathematics.lean
17	Mathlib	Mathlib.lean
18	Verification	Verification.lean, GameOfLife.lean, StackMachine.lean
19	AI
20	References

Build

git clone https://github.com/sdiehl/zero-to-qed
cd zero-to-qed
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
cargo install mdbook

And then...

just build          # Build Lean project
just test           # Run tests
just run            # Run executable
just serve          # Serve docs locally
just build-docs     # Build documentation
just dev            # Lint, build, test
just ci             # Full CI checks
just clean          # Clean build artifacts
just update         # Update dependencies
just stats          # Project statistics

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.