Introduction

Welcome to From Zero to QED, an informal introduction to formality in Lean 4. This article series teaches the language from first principles. Lean is expressive but the learning resources remain scattered and incomplete. This series is a best effort to fill that gap.

Read Online | Download PDF

Note

This is the beta release. There are bound to be typos, errors, and rough edges. If you spot something, send a PR on GitHub.

Tip

This article is itself a giant checkable theorem. Every code sample, every proof, every definition is extracted from source files that the Lean compiler typechecks on every build. If the article compiles, the theorems are valid. The full source lives in the GitHub repository.

What This Series Covers

The series divides into two arcs. The first arc treats Lean as a programming language. You will learn the syntax, type system, control flow, polymorphism, monads, and IO. By the end of this arc you can write real programs in Lean.

The second arc treats Lean as a theorem prover. You will learn to write proofs, understand type theory and dependent types, master tactics, and eventually prove classic mathematical results. The series concludes with the emerging intersection of theorem proving with artificial intelligence, and why formal methods may matter more in the coming decade than they have in the previous five.

No prior experience with theorem provers is assumed. Familiarity with a typed functional language like Haskell, OCaml, or Scala helps but is not strictly required.

Getting Started

There are several ways to follow along with the examples, from zero-install browser options to full local setup.

Option 1: Browser

Lean Live runs Lean 4 in your browser with no installation. Copy code snippets from the text and paste them into the editor. For compatibility with examples in this series, set the toolchain to leanprover/lean4:v4.24.0 and Mathlib to v4.24.0 in the settings. Some later chapters require Mathlib, which Lean Live supports but loads slowly on first use.

Option 2: One-Click Cloud Environment

Launch a complete Lean 4 environment in your browser with no local setup:

• Open in GitHub Codespaces - Free for 120 core-hours/month
• Open in Gitpod - Free tier available

Both options provide VS Code in the browser with Lean 4, the language extension, and all dependencies pre-installed. The environment runs lake exe cache get automatically on startup to download prebuilt Mathlib artifacts.

Option 3: Dev Container (Docker + VS Code)

If you have Docker and VS Code installed locally, clone the repo and open it in VS Code:

git clone https://github.com/sdiehl/zero-to-qed
code zero-to-qed

VS Code will detect the .devcontainer configuration and prompt you to “Reopen in Container”. This builds the same environment locally, giving you cloud-like convenience with local performance.

Option 4: Local Installation

For the full experience, install Lean 4 with VS Code and the Lean 4 extension. Other editors work too (Zed, Emacs, Neovim all have Lean support) but VS Code is the best documented and most widely used. Clone the repository:

git clone https://github.com/sdiehl/zero-to-qed
cd zero-to-qed
lake exe cache get   # Download prebuilt Mathlib (saves hours)
lake build

The lake exe cache get command downloads prebuilt artifacts for Mathlib, reducing the initial build from hours to minutes. Without it, Lake compiles Mathlib from source, which tests your patience more than your code.

You can also serve the documentation locally with just serve if you have mdBook installed.

Repository Structure

Code samples are extracted from Lean source files. Each chapter corresponds to modules in the src/ directory:

Larger examples live in src/Examples/:

Open these files in VS Code to explore with full IDE support. The Infoview panel shows types and proof states as you navigate.

Additional learning resources are collected in the References appendix. This series is an informal introduction to formality. If you want the stuffy formal introduction to formality, see Theorem Proving in Lean 4, Functional Programming in Lean, Mathematics in Lean, or university courses from CMU, Imperial, and Brown. They are more rigorous.