⊢ Compiler-backed Lean execution

Check a Lean file in the environment it needs.

Lean Runtime resolves one exact environment — toolchain and dependencies — runs Lean inside it, 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

The model

Four nouns and one rule.

Context

Where requirements come from

--using, frontmatter, the owning Lake project, or automatic discovery — in that order.

Environment

One exact, immutable set

A toolchain plus every package at a pinned revision. Identified by content, never by a mutable tag.

Lock

An environment written down

Reusable on any machine, including with network access disabled.

Verdict

Lean's answer

accepted or rejected, always inside one named environment. A rejection is a normal result.

Discovery proposes an environment. Only Lean accepts it. status shows the proposal; check produces the verdict.

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