Lean Runtime

Run Lean proofs from Python or a single .lean file—without creating a throwaway Lake project or rebuilding the same dependencies on every machine.

Lean Runtime discovers the exact Lean environment a project needs and reuses a downloadable copy when one is available. It returns structured Lean results with a record of the toolchain and dependencies that were actually used.

Status: V1 beta. The local backend runs trusted Lean, Lake, and package code; it is an orchestration boundary, not a security sandbox.

Install

python -m pip install lean-runtime

Lean Runtime manages its own Elan installation on macOS and Linux. Windows currently requires LEAN_RUNTIME_ELAN.

Run one Lean file

Inside an existing pinned Lake project, just pass the file:

lean-run MyProject/Main.lean

Standalone files do not need a throwaway Lake project or dependency declaration:

import Mathlib

example : 2 + 2 = 4 := by norm_num

lean-run Main.lean

When no explicit context or pinned Lake project exists, lean-run analyzes imports, ranks a bounded set of exact environments from its bundled catalog, and asks Lean to check each candidate. The successful exact lock is retained by Runtime. Pin it for portable reuse whenever desired:

lean-run Main.lean --lock-out environment.lock.json
lean-run Main.lean --lock environment.lock.json

The bundled catalog covers Mathlib v4.30.0 through v4.33.0 and matching LeanCert releases, plus core Lean v4.32.2. Runtime first tries its local store and downloadable environment libraries, then builds the exact source environment when necessary. Use --no-source-build to forbid that potentially large fallback or --offline to use retained environments only.

Before a cold run, inspect its cost without changing the store:

lean-run Main.lean --plan
lean-run Main.lean --max-download 2GiB

New-format libraries publish two independently verified pieces: a slim Lean check runtime and seekable module packs. Lean Runtime computes the source's transitive import closure, downloads only the corresponding compressed frames, and shares verified module artifacts across Mathlib, LeanCert, and future environments. A warm check is silent apart from its result. Older published environments remain readable and automatically use the legacy full-bundle path, so this optimization does not invalidate existing locks.

Explicit frontmatter remains available when the desired context is already known:

-- /// lean-runtime
-- requires = ["mathlib@v4.33.0"]
-- ///

import Mathlib

The same context can be supplied from the command line:

lean-run Main.lean --with mathlib@v4.33.0

Create an exact lock from an explicit dependency for CI without changing the file:

lean-run Main.lean --with mathlib@v4.33.0 \
  --lock-out environment.lock.json
lean-run Main.lean --lock environment.lock.json

Python

Configure an environment once, then use it repeatedly:

import lean_runtime as lean

env = lean.setup(["mathlib@v4.33.0"])

result = env.check(
    """
    import Mathlib
    example : 2 + 2 = 4 := by norm_num
    """
)
result.raise_for_error()

Rejected proofs carry parsed diagnostics:

result = env.check(broken_proof)

for error in result.errors:
    print(error.file, error.line, error.message)

result.raise_for_error()  # raises LeanCheckError with the same detail

Core-only work does not need a dependency:

core = lean.setup(toolchain="v4.32.2")
core.check("example : 2 + 2 = 4 := rfl").raise_for_error()

Batch and asyncio APIs reuse that prepared environment:

results = env.check_many(generated_proofs, concurrency=8)
results = await env.check_many_async(generated_proofs, concurrency=20)

Local projects use the same setup pattern while retaining mutable-project semantics:

project = lean.setup(project="./my-project")
result = project.check_file("./my-project/MyProject/Main.lean")

Create a normal Lake project. The newest stable cataloged Mathlib is the default, and exact dependencies are shared automatically:

lean-runtime init MyProof
cd MyProof
lean-runtime check MyProof/Basic.lean
lean-runtime check MyProof/Basic.lean --watch
# Check every declared local library, in Lake dependency order:
lean-runtime check
lean-runtime build

init also writes an AGENTS.md with the project build, checking, dependency, and shared-package rules for coding agents. Pass --no-agents to omit it; an existing AGENTS.md is never overwritten. Use --core for no Mathlib, or --mathlib-version 4.33.0 to select a cataloged release. lean-runtime update explicitly moves a project to the newest cataloged Mathlib after a preview.

Running lean-runtime init . in an existing pinned Lake project adopts its current exact graph without running lake update. If you already have many Lake checkouts, register them once as local dependency seeds:

lean-runtime scan ~/research
lean-runtime init .

init --plan is side-effect free; --max-download 500MiB and --offline enforce cold-start policy. Advanced bulk migration remains available through attach, and detach --execute materializes an independent project again. For a new project, the target may be absent, empty, or an otherwise empty Git repository root; existing Git identity and index state are preserved. A custom AGENTS.md is also allowed and retained. Other existing contents are rejected before acquisition rather than overwritten. An existing target directory remains the same live directory, so init . does not invalidate the invoking shell's working directory. When the directory spelling is not the intended Lean module capitalization, set it explicitly, for example lean-runtime init . --name IntegralFramework.

One-shot helpers are available when setup reuse is unnecessary:

result = lean.check(source, deps=["mathlib@v4.33.0"])
result = lean.check_file("./my-project/MyProject/Main.lean")

When you need evidence rather than extra setup, the operations CLI can verify, explain, compare, and measure the same exact contexts:

lean-runtime verify research-stack --offline
lean-runtime compare previous.lock.json environment.lock.json
lean-runtime profile research-stack Main.lean --repeat 5
lean-runtime matrix compatibility.toml Main.lean

Use lean-run Main.lean --explain to inspect context routing without executing Lean, and --timings to expose preparation versus execution time. Successful ordinary checks remain one concise line.

Friendly references remain exact: use mathlib@VERSION, leancert@VERSION, owner/repository@REVISION, or the explicit github:owner/repository@REVISION form. Bare floating package names are never accepted.

Share environments

A project is your ordinary Lake repository. Its environment is the exact Lean version, dependencies, and build configuration needed to use it. A downloadable environment is a ready-to-use copy that collaborators and CI can fetch instead of rebuilding Mathlib.

Environment libraries may be public or private. For example:

lean-runtime --library ghcr.io/owner/lean-environments download environment.lock.json
lean-runtime publish environment environment.lock.json \
  --publish-to ghcr.io/owner/lean-environments

Publication verifies push access before doing an expensive build and reports which credential source it selected. Run lean-runtime publish environment --publish-to ghcr.io/owner/lean-environments --check-access to test access by itself. A registry denial is a nonzero, machine-distinct failure; success is not reported until the remote manifest digest is read back and verified.

To publish an existing clean Git-backed Lean project, inspect it and generate the maintained multi-platform workflow:

lean-runtime project inspect . --module MyProject
lean-runtime project init-publish . \
  --module MyProject \
  --library ghcr.io/owner/my-project-environments

The workflow builds and verifies Linux and macOS environments, finalizes the environment and slim-toolchain indexes atomically, then checks clean consumers. For a one-machine handoff, lean-runtime project export writes a source-free portable capsule containing only the selected public module's closure. See Publishing a Lean project.

For an already-built executable, Lean Runtime can also create a verified ready-to-run program. It opens without rebuilding the project, can be saved as a portable copy, and can be shared through a public or private program library. See Ready-to-run programs.

Technical details

The simple API is backed by exact Git commits and trees, Lake-resolved locks, platform-aware content-addressed environments, atomic cross-process builds, downloadable environment reuse, sparse content-addressed module packs, replayable provenance, verification, and trusted publishers. The libraries use OCI-compatible storage internally, but users do not need Docker or container concepts. Advanced protocol details remain in the architecture documentation.

Documentation

• Getting started
• Python API
• lean-run and operations CLI
• Managed environments
• Local Lake projects
• Publishing a Lean project
• Portable copies and environment libraries
• Ready-to-run programs
• Architecture
• Trust and limitations
• V1 release case study

License

Apache License 2.0.