This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.

Jump to the corresponding page on the main Lean 4 website.

Installing Lean 3 and mathlib on Windows #

This document explains how to get started with Lean 3 and mathlib.

If you get stuck, please come to the chat room to ask for assistance.

There is a video walkthrough of these instructions on YouTube.

We'll need to set up Lean, an editor that knows about Lean, and mathlib (the standard library). Rather than installing Lean directly, we'll install a small program called elan which automatically provides the correct version of Lean on a per-project basis. This is recommended for all users.

Installing elan #

  1. We'll need a terminal, along with some basic prerequisites.

    We recommend that you use git bash and not msys2, since installing the supporting tools (below) causes issues in msys2.

    Install Git for Windows (you can accept all default answers during installation). Then open a terminal by typing git bash in the Windows search bar.

  2. In terminal, run the command

    curl -sSf | sh

    and hit enter when a question is asked. To make sure the terminal will find the installed files, run echo 'PATH="$HOME/.elan/bin:$PATH"' >> "$HOME/.profile".

    Then close and reopen Git Bash.

Installing mathlib supporting tools #

In order to use mathlib supporting tools, you need to get python first.

Get Python #

Configure Git #

Get Scripts #

Then, at a terminal, run the command

pip3 install mathlibtools

Installing and configuring an editor #

There are two Lean-aware editors, VS Code and emacs. This document describes using VS Code (for emacs, look at

  1. Install VS Code.
  2. Launch VS Code.
  3. Click on the extension icon (image of icon) (or (image of icon) in older versions) in the side bar on the left edge of the screen (or press ShiftCtrlX) and search for leanprover.
  4. Select the lean extension (unique name jroesch.lean). There is also a lean4 extension, but that one isn't relevant here.
  5. Click "install" (In old versions of VS Code, you might need to click "reload" afterwards)
  6. Setup the default profile:
    • If you're using git bash, press ctrl-shift-p to open the command palette, and type Select Default Profile, then select git bash from the menu.
    • If you're using msys2, press ctrl-comma again to open the settings, and add two settings:
      "": "C:\\msys64\\usr\\bin\\bash.exe",
      "": ["--login", "-i"]
  7. Restart VS Code.

Lean Projects #

You can now read instructions about creating and working on Lean projects