In this guide you will install Lean 4, clone the lean-spec repository, open it in Visual Studio Code, and write your first formal program specification using Lean’s dependent type system. By the end you will have a working Lean file that defines a specification, an implementation, and a machine-checked verification that the implementation meets the specification — all in fewer than ten lines of code.Documentation Index
Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt
Use this file to discover all available pages before exploring further.
Install Lean 4
Follow the official Lean 4 setup instructions to install When you open the project,
elan (the Lean version manager) and the Lean 4 toolchain.The lean-spec repository includes a lean-toolchain file at the root that pins the exact Lean version used by the tutorial:elan reads this file and automatically downloads and activates the correct toolchain — you do not need to manage versions manually.Clone the Repository
Clone the lean-spec repository from GitHub:The repository layout is:
The project depends on two Lake packages declared in
| Path | Contents |
|---|---|
LeanSpec/ | Lean source files (the actual specifications) |
md/ | Generated markdown documentation |
lean-toolchain | Pins the Lean version via elan |
lakefile.lean | Lake build configuration |
lake-manifest.json | Locked dependency versions |
lake-manifest.json:stdfrom leanprover/std4 — the Lean 4 standard library, providing collection types, algorithms, and utilities used throughout the specifications.mdgenfrom Seasawher/mdgen — the tool used to generate themd/documentation from the Lean source files.
Open in VS Code
Open the cloned directory in Visual Studio Code:If you have the Lean 4 VS Code extension installed, it will detect the
lean-toolchain file (leanprover/lean4:v4.5.0-rc1) and activate the correct Lean toolchain automatically.Open any file under LeanSpec/ — for example LeanSpec/Introduction.lean — and the Lean server will start. You will see blue squiggles while the server initialises, which resolve once the file is checked. The Lean Infoview panel (opened with Ctrl+Shift+Enter / Cmd+Shift+Enter) shows types, goals, and #check / #eval output inline.Your First Specification
The canonical introductory example in lean-spec is specifying a function that doubles a natural number. Work through this progression to understand how propositions, types, and subtypes relate.Step 1 — A proposition (no computational content):The implementation returns a subtype structure with two fields:Place your cursor after the This is machine-checked evidence that Lean outputs
DoubleProp is a valid Lean proposition, but propositions have no computational content. You could prove it, but you cannot evaluate it or use it as a type signature for a function without a separate proof step.Step 2 — A subtype specification (the right approach):Double₃ is a type — specifically, for each n, it is the subtype of natural numbers m for which m = 2 * n holds. A function whose return type is Double₃ n is a function that must return a value together with machine-checked evidence that the value is twice n. This is the specification.Step 3 — An implementation:val— the computed value2 * n.property— evidence thatval = 2 * n, discharged here byrfl(reflexivity, since2 * n = 2 * nis definitionally true).
#check line in VS Code. The Lean Infoview will confirm:double implements Double₃ for every n.Step 5 — Evaluate:8. The non-computational content (the property field) is erased at evaluation time — you get a plain natural number, with no runtime overhead from the specification machinery.Build the Markdown Documentation
The This processes all files under
md/ directory contains documentation generated from the Lean source files using the mdgen tool. To regenerate it after making changes to the Lean sources, run:LeanSpec/, extracts the documentation comments (written in /-! ... -/ and /- ... -/ blocks), and produces corresponding .md files under md/. The Lean code blocks in the source become fenced code blocks in the output.Key Lean Concepts
The specifications in lean-spec are built from a small vocabulary of Lean logic and type constructs. The following tables summarise the most important ones, drawn directly fromLeanSpec/Introduction.lean.
Logical Connectives and Quantifiers
These are the building blocks of propositions in Lean’s logic:| Notation | Meaning |
|---|---|
P ∧ Q | Conjunction — both P and Q hold |
P ∨ Q | Disjunction — at least one of P or Q holds |
P → Q | Implication — if P then Q |
P ↔ Q | Logical equivalence — P if and only if Q |
¬ P | Negation — P does not hold |
∀x, P x | Universal quantification — P x holds for all x |
∃x, P x | Existential quantification — there exists an x such that P x holds |
True | The always-true proposition |
False | The never-true proposition |
Core Types
These are the types used to construct specifications:| Notation | Meaning |
|---|---|
T × U | Cartesian product — pairs of a T and a U |
T ⊕ U | Disjoint union — a value that is either a T or a U |
T → U | Function type — functions from T to U |
Nat | Natural numbers (0, 1, 2, …) |
String | Character sequences |
List T | Finite sequences of elements of type T |
(a : A) → B a | Dependent function type — corresponds to ∀ |
(a : A) × B a | Dependent product type — corresponds to ∃ |
{ a : A // P a } | Subtype — elements of A satisfying proposition P |
T → U and T × U are degenerate cases of (a : A) → B a and (a : A) × B a respectively, where B does not depend on a. The subtype { a : A // P a } is the workhorse of lean-spec: it bridges the gap between types (which have computational content) and propositions (which do not), making it the natural tool for expressing what a function must return.
Naming conventions. Lean-Spec follows standard Lean naming conventions: type and proposition names are camel case with an initial upper case letter (e.g.
Double₃, DoubleProp), while function names are camel case with an initial lower case letter (e.g. double). Subscript numerals (e.g. Double₁, Double₂, Double₃) are used within the tutorial to distinguish successive refinements of the same definition.Next Steps
Lean as a Spec Language
Understand how Lean’s logic and type system combine to create a single unified specification, programming, and proof language.
Types and Propositions
Explore the Curry–Howard correspondence and why the distinction between types and propositions matters for specification.
Subtypes and Dependent Types
Master the subtype
{ a : A // P a } and the dependent function and product types — the core tools of lean-spec.