⊢ Compiler-backed Lean execution

Check a Lean file in the environment it needs.

Lean Runtime resolves an exact toolchain and dependency context, runs Lean, and records what actually ran.

Run your first check How context is selected

python -m pip install lean-runtime Copy

Python 3.10 or newer and Git are required. Automatic Elan bootstrap is available on macOS and Linux.

Automatic Pinned Lake project

Primes.lean standalone file

import Mathlib.Data.Nat.Prime.Infinite

example : ∀ n : ℕ, ∃ p, n ≤ p ∧ p.Prime :=
  Nat.exists_infinite_primes

terminal ready

↻ Replay Inspect this run

Workflows

Use the entry point that matches your work.

Standalone file

Bring a Lean source file

lean-runtime check Main.lean

Lean Runtime discovers a plausible exact environment and accepts it only when Lean accepts the file.

Check Lean files

Lake project

Keep the project authoritative

lean-runtime adopt . --yes
lean-runtime build

The project keeps its pinned toolchain and manifest. Dependency storage and compatible artifacts can be reused.

Work with Lake projects

Exact and offline

Record the environment

lean-runtime check Main.lean \
  --write-lock environment.lock.json

Reuse the resulting lock explicitly, including with network access disabled.

Use an exact lock