1 Installing Lean🔗

The recommended setup is Lean 4 with Visual Studio Code:

• Install Visual Studio Code.

• Install the official Lean 4 VS Code extension. In VS Code, open the Extensions sidebar, search for Lean 4, and install the extension published by leanprover.

• Follow the Lean quickstart to create or open a Lean project. The extension will guide you through installing the Lean toolchain using elan if it is not already installed.

After installation, open a .lean file in VS Code and check that the Lean infoview appears. You can also confirm the command-line tools with lean –version and lake –version.