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

For a portable standalone file, declare exact dependencies in TOML frontmatter:

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

import Mathlib

example : 2 + 2 = 4 := by norm_num

lean-run Main.lean

The same context can be supplied from the command line:

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

Create an exact lock for CI without changing the file:

lean-run Main.lean --with mathlib@v4.32.2 \
  --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.32.2"])

result = env.check(
    """
    import Mathlib
    example : 2 + 2 = 4 := by norm_num
    """
)
result.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")

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

result = lean.check(source, deps=["mathlib@v4.32.2"])
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 build-and-publish environment.lock.json \
  --publish-to ghcr.io/owner/lean-environments

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, 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

License

Apache License 2.0.

Project links

Data verified by PyPI on Aug 5, 2026
Data provided by the project maintainers, verified at the time the release was uploaded to PyPI.

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Newer release available (4.22.0)

1 maintainer

PyPI data
Data sourced directly from PyPI's database.
Avatar for alerad from gravatar.com alerad

Credits

Author: Alejandro Radisic

GitHub Statistics

Data verified by PyPI on Aug 5, 2026
The GitHub source repository was provided by the project maintainers and verified by PyPI at the time of upload. Stars, forks, and open issues/PRs are derived from that repository and have not been independently verified.

License expression

Apache-2.0
View SPDX License List

Requires

Python >=3.10

Provides Extra

dev docs

Tags

lean4 theorem-prover formal-verification toolchain

Classifiers

Report project as malware

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

lean_runtime-2.0.0.tar.gz (143.7 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

lean_runtime-2.0.0-py3-none-any.whl (110.8 kB view details)

Uploaded Python 3

File details

Details for the file lean_runtime-2.0.0.tar.gz.

File metadata

  • Download URL: lean_runtime-2.0.0.tar.gz
  • Upload date:
  • Size: 143.7 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for lean_runtime-2.0.0.tar.gz
Algorithm Hash digest
SHA256 347f68d76cd3ebb98936596497b4dd0d0d399409b073b56eb8d888503c93fa0c
MD5 d022889ba5a540ca8eda1dfc3f1eefee
BLAKE2b-256 f758ed27b73b8cf47e8c26fe2c7e3d9f8b5ad2577375708bb36724e7721f4251

See more details on using hashes here.

Provenance

The following attestation bundles were made for lean_runtime-2.0.0.tar.gz:

Publisher: release.yml on alerad/lean-runtime

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file lean_runtime-2.0.0-py3-none-any.whl.

File metadata

  • Download URL: lean_runtime-2.0.0-py3-none-any.whl
  • Upload date:
  • Size: 110.8 kB
  • Tags: Python 3
  • Uploaded using Trusted Publishing? Yes
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for lean_runtime-2.0.0-py3-none-any.whl
Algorithm Hash digest
SHA256 2589b38bcbd03855e7958a19b687df05587e943611266812b2e21d7ff5e08e33
MD5 4de8277bfb3c8155073494da89fe2329
BLAKE2b-256 e09b7cc639725ededf260519d4c43974b8399cea193ae4094f26fad1015a94c0

See more details on using hashes here.

Provenance

The following attestation bundles were made for lean_runtime-2.0.0-py3-none-any.whl:

Publisher: release.yml on alerad/lean-runtime

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Release history Release notifications | RSS feed

4.22.0

2 files

4.21.0

2 files

4.2.0

2 files

4.1.1

2 files

4.1.0

2 files

4.0.1

2 files

4.0.0

2 files

3.0.3

2 files

3.0.2

2 files

3.0.1

2 files

3.0.0

2 files

2.10.0

2 files

2.9.2

2 files

2.9.1

2 files

2.9.0

2 files

2.8.0

2 files

2.7.0

2 files

2.6.2

2 files

2.6.1

2 files

2.6.0

2 files

2.5.0

2 files

2.4.0

2 files

2.3.0

2 files

2.2.0

2 files

2.1.2

2 files

2.1.1

2 files

2.1.0

2 files

2.0.9

2 files

2.0.8

2 files

2.0.7

2 files

2.0.6

2 files

2.0.5

2 files

2.0.3

2 files

2.0.2

2 files

2.0.1

2 files

This release

2.0.0 This release

2 files

1.0.0

2 files

0.6.0

2 files

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page