An informal introduction to formality in Lean 4.
- HTML - Read online
- PDF - Download for offline reading
No local setup required. Launch a complete Lean 4 environment in your browser:
The environment comes pre-configured with Lean 4, the VS Code extension, and all dependencies.
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.
| # |
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 |
|
See BUILD.md for details on the HTML and PDF build pipeline. Add yourself to CONTRIBUTORS.md and submit a PR.
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.