1.1 Installation and Toolchain

Lean is distributed as a small toolchain rather than as a single editor plugin. The main pieces are the Lean compiler, the Lake build tool, the package manager configuration, and the editor integration. In normal use you install Lean once, create or open a Lake project, and let the project decide which Lean version it uses.

This recipe sets up a working Lean environment and checks that the toolchain can compile, run, and typecheck a small file.

Problem

You want a clean Lean installation that can create projects, fetch dependencies, build code, and work with an editor.

Solution

Install elan, the Lean version manager. Then use it to install Lean and Lake.

On macOS or Linux, the usual installation path is:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

After installation, open a new terminal and check the tools:

lean --version
lake --version
elan --version

Create a new project:

lake new hello
cd hello
lake build

Create a file named Hello.lean or edit the generated main file, depending on the project template:

def main : IO Unit := do
  IO.println "hello, Lean"

Run it:

lake exe hello

For editor support, install Visual Studio Code and the Lean 4 extension. Open the project directory, not just a single .lean file. Lean needs the project root so that imports, dependencies, and build configuration are resolved correctly.

Discussion

Lean projects are versioned environments. The Lean version used by a project is usually recorded in a file named lean-toolchain. A typical file contains a single line such as:

leanprover/lean4:stable

or a specific version:

leanprover/lean4:v4.12.0

When you enter the project directory and run lean, lake, or use the editor, elan reads this file and selects the matching Lean toolchain. This is important because Lean code can depend on exact elaboration behavior, library names, and tactic behavior. A project should compile with the Lean version it was written for.

Lake is the build tool for Lean projects. It plays the same practical role that cargo plays for Rust or go commands play for Go projects. It describes packages, libraries, executables, dependencies, and build targets. In a small project, you may only use:

lake build

to compile everything, and:

lake exe name

to run an executable. In a larger project, Lake also manages dependencies such as mathlib.

Lean itself can check a single file:

lean MyFile.lean

but cookbook-style Lean development should usually happen inside a Lake project. A project gives you stable imports, predictable dependencies, and reproducible builds.

Minimal Example

A minimal theorem can be checked without writing an executable:

theorem identity_example (P : Prop) : P -> P := by
  intro h
  exact h

This says that for every proposition P, if P holds, then P holds. The proof introduces the hypothesis h : P and then uses exactly that hypothesis to solve the goal.

A minimal computed definition looks like this:

def double (n : Nat) : Nat :=
  n + n

#eval double 21

The command #eval double 21 asks Lean to compute the expression. It should display:

Common Pitfalls

If the editor cannot find imports, open the whole project folder instead of an individual file.

If lake build uses the wrong Lean version, inspect lean-toolchain.

If a command works in one project but fails in another, compare their Lean versions and dependencies.

If lake exe hello fails, check the executable name in lakefile.lean.

If the Lean extension appears stuck, run:

lake build

from the terminal first. Build errors are often easier to read there.

Takeaway

A Lean installation consists of elan, lean, lake, and editor support. For ordinary work, create a Lake project, let lean-toolchain control the Lean version, and use the editor inside the project root. This gives you a reproducible environment for definitions, proofs, executables, and later dependency management.