An informal introduction to formality in Lean 4.
- HTML - Read online
- PDF - Download for offline reading
Follow the official Lean installation instructions.
| # | 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 | |
| 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.
