3. Installing Lean🔗

3.1. What is Lean?🔗

Lean is a programming language and a theorem prover. In this guide we will use it mainly as a theorem prover: a system in which mathematical statements and proofs are written in a language precise enough for a computer to check them. If Lean accepts a proof, then the proof follows from the definitions, lemmas, and axioms that were used to write it.

When we say that we are going to install Lean, we mean that we are going to put the Lean tools on our own computer. This includes the program that checks Lean files, the tools that manage Lean projects, and the editor integration that lets us write Lean code comfortably. After installation, Lean will be available locally, just like any other program installed on the system.

There are also online ways to try Lean in a browser. They are useful for testing small examples, following a tutorial, or getting a first impression without installing anything. They are not enough for our purposes, however. We are going to use LLMs to write and modify Lean code inside real projects. That workflow has to happen locally, on the same machine where the project lives.

How does Lean check proofs?

When Lean reads a file, it first parses the text and then elaborates it. Elaboration is the process of turning the convenient language that we write into a fully explicit internal term. For instance, Lean has to infer implicit arguments, insert coercions, resolve typeclass instances, expand notation, and translate tactic proofs into ordinary proof terms.

The central point is that these generated terms are then checked by a small trusted part of Lean, called the kernel. A theorem statement is a type, and a proof is a term of that type. The kernel checks that the term really has the required type. Tactics, automation, and LLMs may help us construct the term, but they do not get to decide whether the proof is correct: the kernel still checks the result.

When a file is accepted, Lean also compiles the declarations it contains. For theorem proving, the most important compiled files have the extension .olean. A .olean file records the checked definitions, theorem statements, proof terms, typeclass instances, notation, and other information produced from a Lean source file. When another file imports that module, Lean can load this compiled information instead of parsing and elaborating the original source file again. This is what lets a large library be built in pieces instead of checking everything from scratch every time.

You can find the full details of elaboration, reduction, tactics, compilation, and the kernel in the Lean language reference.

3.2. How to install Lean🔗

The official installation instructions can be found here. They consist of three simple steps. Even though they are quite straightforward, let us make some further comments on them to better understand what is going on.

Installation instructions

Install VS Code. Clicking the button Install VS Code will redirect you to the official VS Code download page. This website will try its best to show you, by default, the download button corresponding to your operating system (in my case, GNU/Linux). You have to download and then install this program, following the standard procedure of your operating system (usually this means just downloading the file and clicking on it to start the installer).

Why install VS Code? I thought we were going to install Lean!

VS Code is an integrated development environment, or IDE. A plain text editor lets you open a file and write text in it. An IDE adds tools for writing code: it highlights the syntax with different colors, reports mistakes, suggests possible completions, helps you jump to definitions, and gives information that helps you understand and debug errors.

This is especially useful for Lean. When we write Lean code, we do not just want to edit text: we want to see whether Lean accepts the statement or proof, inspect the current proof state, jump to definitions, and get feedback while we are writing. VS Code gives us a comfortable place where all this information can appear next to the file we are editing.

VS Code is also extensible. This means that it can be expanded by installing small packages called extensions. The Lean extension is what teaches VS Code how to work with Lean files. Without it, VS Code would just see a Lean file as ordinary text.
If you are using Windows...

After installing VS Code, open the Windows terminal (not the WSL terminal!) and run:
$
```
code --install-extension ms-vscode-remote.remote-wsl
```
Now open the WSL terminal and run
```
code .
```
This will open VS Code through WSL, so that afterwards, when we open a terminal inside VS Code, it will use WSL. From now on, whenever you want to open VS Code, you have to do it this way to guarantee that all the set up we will be doing in this chapter is available.

In particular, make sure to keep this VS Code session open, so that when below you click on links, those links are opened in this particular VS Code window (and not in a new one).
Beyond VS Code

VS Code is the recommended option because it is the easiest path to set up and the one assumed by the official Lean installation guide. It is not the only possible editor.

Lean can also be used from editors such as NeoVim or Emacs. These are very configurable text editors, popular among people who like to work mainly from the terminal or who want to customize every part of their editing environment. With the right Lean integration, they can also show Lean errors, proof states, definitions, and other useful information. If you already use one of them, you can use it for Lean too. If you do not, VS Code is the simplest place to start.
Install the extension. Once VS Code is installed, we have to install the Lean 4 extension, to have all the necessary tools to write Lean 4 available in VS Code. For this we just have to click the button Get the extension. If we have VS Code properly installed, this will open the program and show us the Lean 4 extension homepage. We just have to click Install. Now VS Code is ready to handle Lean.
Complete the extension setup. Now we are going to truly install Lean. As before, click the Open setup guide button. This will open a VS Code guide that will walk you through the necessary VS Code setup. The important point of the setup is Install Lean. Go there and click Click to install. If everything goes smoothly, this should install Lean on your system.

Most people need to reboot their computers at this point for Lean to actually work.

At this point, we could start our own Lean project. Our goal, however, is to contribute to an existing library to add the necessary infrastructure (i.e., preliminary results) to be able to formalize the theorems in our own research. Let's find out what such a library is, and how to contribute to it.