These instructions will walk you through setting up Lean using the "basic" setup and VS Code as the editor. See Setup for other ways, supported platforms, and more details on setting up Lean.
See quick walkthrough demo video.
Install VS Code.
Launch VS Code and install the
Create a new file using "File > New Text File" (
Ctrl+N). Click the
Select a languageprompt, type in
lean4, and hit ENTER. You should see the following popup:
Click the "Install Lean using Elan" button. You should see some progress output like this:
info: syncing channel updates for 'nightly' info: latest update on nightly, lean version nightly-2021-12-05 info: downloading component 'lean'
While it is installing, you can paste the following Lean program into the new file:
When the installation has finished, the Lean Language Server should start automatically and you should get syntax-highlighting and a "Lean Infoview" popping up on the right. You will see the output of the
#evalstatement when you place your cursor at the end of the statement.
You are set up!
You can now create a Lean project in a new folder. Run
lake init foo from "View > Terminal" to create a package, followed by
lake build to get an executable version of your Lean program.
On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
Note: Packages have to be opened using "File > Open Folder..." for imports to work.
Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (
The InfoView says "Waiting for Lean server to start..." forever.
Check that the VS Code Terminal is not showing some installation errors from
If that doesn't work, try also running the VS Code command
Developer: Reload Window.