För att installera Lean 4 i macOS-miljö (under antagande om att brew redan finns installerat):
% brew update
% brew install elan-init
% elan toolchain install nightly
% elan default nightly
% lean --version
…
Lean (version 4.16.0-nightly-2025-01-19, arm64-apple-darwin23.6.0, commit 74bd40d34d1a, Release)
För att installera Lean 4 i Linux-miljö (under antagande om en Debian-baserad distribution, alternativt en temporär Debian-miljö skapad via docker run -it --rm debian:unstable efter att brew install docker --cask körts):
% apt update
% apt install -y elan curl git
% elan toolchain install nightly
% elan default nightly
% lean --version
…
Lean (version 4.16.0-nightly-2025-01-19, aarch64-unknown-linux-gnu, commit 74bd40d34d1a, Release)
För att skapa ett nytt Lean-projekt som använder sig av Mathlib:
% lake new project_name math
% cd project_name/
% lake exe cache get
% echo 'import Mathlib' > ProjectName/Basic.lean
% echo 'example : 1 + 1 != 3 := by aesop' >> ProjectName/Basic.lean
% lake build
För att installera VS Code samt Lean-stöd:
# Installera VS Code
% brew install --cask visual-studio-code
# Installera Lean-stöd i VS Code
% code --install-extension leanprover.lean4
…
Extension 'leanprover.lean4' v0.0.186 was successfully installed.
För att installera exempelprojektet ”Formalising Mathematics 2024” (Kevin Buzzard):
% git clone https://github.com/ImperialCollegeLondon/formalising-mathematics-2024.git
% cd formalising-mathematics-2024/
% lake exe cache get
% code .
# Öppna första uppgiften FormalisingMathematics2024/Section01logic/Sheet1.lean
Lean 4 på svenska 