Installing Lean and mathlib on Windows #

This document explains how to get started with Lean 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 https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -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 https://github.com/leanprover/lean-mode).

  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. Click "install" (In old versions of VS Code, you might need to click "reload" afterwards)
  5. Setup the default shell:
"terminal.integrated.shell.windows": "C:\\msys64\\usr\\bin\\bash.exe",
"terminal.integrated.shellArgs.windows": ["--login", "-i"]
  1. Restart VS Code.
  2. Verify Lean is working, for example by saving a file test.lean and entering #eval 1+1. A green line should appear underneath #eval 1+1, and hovering the mouse over it you should see 2 displayed.

Lean Projects #

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