Setting Up Lean

Quickstart

These instructions will walk you through setting up Lean 4 together with VS Code as an editor for Lean 4. See Setup for supported platforms and other ways to set up Lean 4.

  1. Install VS Code.

  2. Launch VS Code and install the Lean 4 extension by clicking on the 'Extensions' sidebar entry and searching for 'Lean 4'.

    Extension installation

    Installing the vscode-lean4 extension

  3. Open the Lean 4 setup guide by creating a new text file using 'File > New Text File' (Ctrl+N / Cmd+N), clicking on the ∀-symbol in the top right and selecting 'Documentation… > Docs: Show Setup Guide'.

    Setup Guide

    Accessing the setup guide

  4. Follow the Lean 4 setup guide. It will:

    • walk you through learning resources for Lean,

    • teach you how to set up Lean's dependencies on your platform,

    • install Lean 4 for you at the click of a button,

    • help you set up your first project.

    Setup Guide

    The setup guide

Supported Platforms

Tier 1

Platforms built & tested by our CI, available as binary releases via elan (see below)

  • x86-64 Linux with glibc 2.26+

  • x86-64 macOS 10.15+

  • aarch64 (Apple Silicon) macOS 10.15+

  • x86-64 Windows 11 (any version), Windows 10 (version 1903 or higher), Windows Server 2022, Windows Server 2025

Tier 2

Platforms cross-compiled but not tested by our CI, available as binary releases

Releases may be silently broken due to the lack of automated testing. Issue reports and fixes are welcome.

  • aarch64 Linux with glibc 2.27+

  • x86 (32-bit) Linux

  • Emscripten Web Assembly

Setting Up Lean

See also the quickstart instructions for a standard setup with VS Code as the editor.

Release builds for all supported platforms are available at <https://github.com/leanprover/lean4/releases>. Instead of downloading these and setting up the paths manually, however, it is recommended to use the Lean version manager elan instead:

$ elan self update  # in case you haven't updated elan in a while
# download & activate latest Lean 4 stable release (https://github.com/leanprover/lean4/releases)
$ elan default leanprover/lean4:stable

lake

Lean 4 comes with a package manager named lake. Use lake init foo to initialize a Lean package foo in the current directory, and lake build to typecheck and build it as well as all its dependencies. Use lake help to learn about further commands. The general directory structure of a package foo is

lakefile.lean  # package configuration
lean-toolchain # specifies the lean version to use
Foo.lean       # main file, import via `import Foo`
Foo/
  A.lean       # further files, import via e.g. `import Foo.A`
  A/...        # further nesting
.lake/         # `lake` build output directory

After running lake build you will see a binary named ./.lake/build/bin/foo and when you run it you should see the output:

Hello, world!

Editing

Lean implements the Language Server Protocol that can be used for interactive development in Emacs, VS Code, and possibly other editors.

Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).