Table of contents

Ch. 1: Basics →

---

Learning objectives. By the end of this chapter, know why Lean (rather than another proof assistant) is this book’s choice, have a working lake/Lean 4 toolchain and editor set up, and understand why this book builds everything from scratch instead of importing Mathlib from the start.

Sections

1. Why Lean?
2. Installing the toolchain
3. Editor
4. A note on Mathlib

---

Table of contents

Ch. 1: Basics →