Module 1 · Level 1

Installation & Setup

Set up Lean with VS Code, Lake, and the Lean 4 extension. This will give you the interactive Infoview and live feedback.

Install Lean via elan

Use elan to manage Lean toolchains. It works like Rust'srustup.

bash

1# Windows (PowerShell)
2winget install Lean4.elan
3
4# macOS / Linux
5curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh

VS Code Extension

Install the Lean 4 extension from the VS Code marketplace. Once installed, every Lean file gives you inline diagnostics and an Infoview panel.

💡

After installing the extension, open the command palette and run “Lean: Restart File” to refresh the toolchain if needed.

Create a First Project

Create a new project with lake and open it in VS Code.

bash

1mkdir lean-playground
2cd lean-playground
3lake init hello
4code .

Exercise: Verify Your Setup

Open Main.lean and add an #eval line. If the Infoview shows the result, your setup works.

lean

1#eval "Lean is ready"

Key Takeaway

The fastest way to learn Lean is to keep the editor open, run small snippets, and read the Infoview after every change.

Back: What is Lean?Next: The Infoview