Skip to main content

Documentation Index

Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt

Use this file to discover all available pages before exploring further.

This guide takes you from zero to a working Lean 4 project in under ten minutes. You will install elan (the Lean version manager), create a new package with lake, run the generated Hello World, write a small function, and prove a theorem about it — all without needing to configure anything by hand.

​
Prerequisites

  • A Unix-like system (Linux, macOS) or Windows with PowerShell
  • An internet connection for downloading the toolchain
  • VS Code (recommended; optional)
1
Install elan
2
elan is the official Lean toolchain manager, similar to rustup for Rust. It downloads and manages Lean versions automatically.
3
Linux / macOS
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Follow the on-screen prompts. When asked for a default toolchain, accept the default (leanprover/lean4:stable). After installation, restart your shell or run:
source ~/.elan/env
Windows (PowerShell)
curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
powershell -f elan-init.ps1
del elan-init.ps1
Restart your terminal after installation.
macOS Homebrew
brew install elan-init
elan-init
4
Verify the installation:
5
lean --version
# Lean (version 4.x.x, ...)
lake --version
# Lake version x.x.x (Lean version 4.x.x)
6
Create a New Package
7
Use lake new to scaffold a new Lean 4 package:
8
lake new hello
cd hello
9
Lake generates the following file structure:
10
hello/
├── Hello/
│   └── Basic.lean      -- Example library module
├── Hello.lean          -- Library root (imports Hello.Basic)
├── Main.lean           -- Executable entry point
├── lakefile.toml       -- Build configuration (TOML format)
└── lean-toolchain      -- Pinned Lean version
11
The lean-toolchain file pins the exact Lean version used by this project. When you open the project in VS Code or run any lake command, elan reads this file and automatically downloads the correct toolchain if it is not already installed.
12
Open Main.lean to see the generated entry point:
13
import «Hello»

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"
14
Hello/Basic.lean contains the library definition used by main:
15
def hello := "world"
16
And Hello.lean is the library root that re-exports Hello.Basic:
17
-- This module serves as the root of the `Hello` library.
-- Import modules here that should be built as part of the library.
import «Hello».Basic
18
Build and Run
19
lake build
lake exe hello
# Hello, world!
20
You can also run the compiled binary directly:
21
./.lake/build/bin/hello
# Hello, world!
22
Open in VS Code
23
Install the Lean 4 extension from the VS Code marketplace (identifier: leanprover.lean4), then open the project folder:
24
code .
25
The extension automatically detects the lean-toolchain file. Open any .lean file and you will see:
26
  • Inline error messages as red squiggles
  • Goal state panel showing the proof state at the cursor
  • Hover info with types and docstrings
  • Go to definition with F12
    • 27
    The first time you open a Lean file, the extension downloads the language server. This can take a minute. Watch the spinning indicator in the status bar.
    28
    Write a Function
    29
    Replace the contents of Hello/Basic.lean with a small library:
    30
    /-- Double a natural number. -/
def double (n : Nat) : Nat := n + n

/-- Triple a natural number. -/
def triple (n : Nat) : Nat := n + n + n

-- Quick evaluation in the editor (hover to see the result)
#eval double 7    -- 14
#eval triple 5    -- 15
    31
    Prove a Property
    32
    Add a theorem below your definitions:
    33
    /-- Doubling is the same as multiplying by two. -/
theorem double_eq_two_mul (n : Nat) : double n = 2 * n := by
  simp [double, Nat.two_mul]

/-- Tripling a number gives a value greater than doubling it (for n > 0). -/
theorem triple_gt_double (n : Nat) (h : 0 < n) : double n < triple n := by
  simp [double, triple]
  omega
    34
    Place your cursor on the by keyword to see the tactic goal state in the Lean Infoview panel on the right.
    35
    -- You can also use #check to inspect types and #print to see definitions
#check double          -- double : Nat → Nat
#print double          -- def double : Nat → Nat := fun n => n + n

    ​
    The lean-toolchain File

    The lean-toolchain file created by lake new contains a single line like: 
    leanprover/lean4:v4.14.0
    This tells elan to use that exact release. To update to a newer release, edit this file or run: 
    elan update
    To pin a specific version for all projects on your machine (as the global default): 
    elan default leanprover/lean4:stable

    ​
    Next Steps

    Installation

    Full installation details including editor setup for Emacs and Neovim.

    Syntax Overview

    Namespaces, imports, sections, and the #check / #eval commands.

    Functions & Definitions

    def, theorem, recursion, implicit arguments, and attributes.

    Inductive Types

    Algebraic data types, pattern matching, and the deriving clause.

    Build docs developers (and LLMs) love

    Get started for freeTalk to us