Lean 4: What It Is, How to Install It and Start a Project

Lean 4 is the current major version of Lean, which its own site describes as a functional programming language and theorem prover built for formalizing math. This guide is for researchers, students and programmers who want to install it, check that it works and start a first project. Everything below follows the official Lean install and documentation pages, read on 2026-11-07.

What Lean 4 is used for in research

Lean is used in two ways: as a programming language, and as a proof assistant in which mathematical statements and proofs are written so the software can check them. The official documentation is organised around those readers rather than around versions of the tool:

Resource (official)	Official description	Start here if you are
Functional Programming in Lean	The main resource for programmers who want to learn Lean; no prior functional programming knowledge is required	A programmer
Theorem Proving in Lean	Designed to teach you to develop and verify proofs in Lean	Learning to write and check proofs
Mathematics in Lean	The main resource for mathematicians who want to learn mathematical formalization, using the Mathlib library	A mathematician
The Lean Language Reference	A comprehensive, precise description of Lean	Looking up exact language behaviour

The Lean documentation page also lists a Lean FAQ and the Mathlib API reference, which covers Lean core, the standard library, Mathlib and other key packages.

Install or access (official source only)

The recommended route on lean-lang.org/install is: install Visual Studio Code, install the extension leanprover.lean4, then run the extension’s setup guide (Documentation > Docs: Show Setup Guide, or the menu behind the top-right forall symbol). The official manual-install page says its steps will not work reliably in every environment and strongly advises the recommended route first. Use the manual route only if you need the command-line tools directly.

Manual install: elan

elan is the Lean version manager; it keeps Lean up to date and selects the version each project needs. lake is Lean’s package manager and build tool and is bundled with Lean.

• Linux and macOS: install git and curl, then run curl https://elan.lean-lang.org/elan-init.sh -sSf | sh. Choose option 1 at the prompt. elan installs to $HOME/.elan and adds a line to $HOME/.profile. To use it in the current terminal run source $HOME/.elan/env.
• Windows: check that git and curl respond in Command Prompt, then run curl -O --location https://elan.lean-lang.org/elan-init.ps1, then powershell -ExecutionPolicy Bypass -f elan-init.ps1, then del elan-init.ps1. Choose 1 at the prompt and close the terminal afterwards.
• VS Code extension from the command line: code --install-extension leanprover.lean4. The page warns that if you leave out leanprover.lean4, the extension is silently not installed. In the VS Code interface you can instead open Extensions (Ctrl+Shift+X), search for lean4 and install the one by leanprover.

Step by step: check the install and start a project

1. Check that Lean runs

1. In VS Code, create a new file named Test.lean and save it. Saving triggers a background install of the full toolchain.
2. Type #eval 1+1 in the file.
3. Hover over #eval; the editor should show the evaluated value.

2. Create and build a Lean project

1. Open a terminal where you want the project folder.
2. Run lake new MyLeanProject.
3. Run cd MyLeanProject && lake build.

3. Create a project that uses Mathlib

1. Run lake +leanprover-community/mathlib4:lean-toolchain new MyMathlibProject math.
2. Enter the new project folder and run lake build. The official page notes the first run may take a while because Mathlib is downloaded.

4. Work on an existing project from GitHub

1. Clone it with git clone https://github.com/<repository owner>/<repository name>.git.
2. If the project depends on Mathlib, or is Mathlib itself, run lake exe cache get.

5. Update Mathlib in a project

Lean itself updates through elan, but Mathlib updates are manual. The official sequence is: curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain, then lake update, then lake exe mk_all && lake build. Afterwards check that your project files still compile.

Output and how to read it

• Editor feedback: a successful #eval 1+1 shows its value when you hover over the command; this is the install check the official page uses.
• Build result: lake build compiles the project. A project whose files still compile after a Mathlib update is the check the official page asks you to make.

For how to read goals, errors and proof states inside a proof, use the exercises in Theorem Proving in Lean or Mathematics in Lean, which are written for that purpose.

Troubleshooting

Symptom	Fix stated on the official manual-install page
lake is an unknown command (Linux, macOS)	Run source ~/.profile or source ~/.bash_profile, then retry
Your distribution suggests sudo apt install elan	Ignore it; add elan to PATH with source $HOME/.elan/env
Extension missing in VS Code, no error shown	Rerun the install with leanprover.lean4 in the code --install-extension command
Commands not found on Windows	Confirm “Add to PATH” was ticked when installing VS Code, and reopen the terminal after installing git or curl
Homebrew VS Code is out of date (macOS)	Homebrew does not auto-update VS Code; run brew update periodically

Lean on its own or with Mathlib

Choice	Create it with	Extra step	Fits
Plain Lean project	lake new MyLeanProject	None beyond lake build	Programming in Lean; learning the language
Lean project with Mathlib	lake +leanprover-community/mathlib4:lean-toolchain new MyMathlibProject math	First build downloads Mathlib; lake exe cache get for cloned Mathlib-dependent projects	Formalizing mathematics (the route Mathematics in Lean uses)

Using Lean 4 alongside reproducible research practice

If you publish Lean code, see how to cite software, code and R packages, the computational reproducibility definition and reproducibility infrastructure for workflows and code sharing. Version control with Git is covered in a researcher’s first GitHub repository, and the general idea of shareable code is defined under open-source software.

FAQ

What is Lean 4?

The current major version of Lean, a functional programming language and theorem prover built for formalizing math, according to lean-lang.org (read 2026-11-07).

How do I install Lean 4?

Install VS Code, install the leanprover.lean4 extension and run its setup guide. For command-line use, install elan, which manages Lean versions per project.

Do I need Mathlib?

Only for projects that use it, such as formalizing mathematics as taught in Mathematics in Lean. A plain project from lake new does not include it.

Which Lean book should I start with?

Functional Programming in Lean for programmers, Mathematics in Lean for mathematicians, Theorem Proving in Lean for learning to develop and verify proofs.

How do I update Lean and Mathlib?

elan keeps Lean up to date automatically. Mathlib is updated manually with the sequence in step 5 above.

Sources (official documentation, read 2026-11-07)

• Lean: Install
• Lean: Manual installation
• Lean: Documentation
• Theorem Proving in Lean 4