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 7, 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 7, 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.3.tar.gz (146.9 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.3-py3-none-any.whl (112.5 kB view details)

Uploaded Python 3

File details

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

File metadata

  • Download URL: lean_runtime-2.0.3.tar.gz
  • Upload date:
  • Size: 146.9 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.3.tar.gz
Algorithm Hash digest
SHA256 8ee4f050a54fa6dafc81e492df618a02cb90c1a4e638f72875daa4c30af18a6b
MD5 8857873b8f23be1ca176e87588367b15
BLAKE2b-256 1172f2148a54b41a473502ed4e1bae15031cfcd2a93ece1a61cfef539b4f8f0a

See more details on using hashes here.

Provenance

The following attestation bundles were made for lean_runtime-2.0.3.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.3-py3-none-any.whl.

File metadata

  • Download URL: lean_runtime-2.0.3-py3-none-any.whl
  • Upload date:
  • Size: 112.5 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.3-py3-none-any.whl
Algorithm Hash digest
SHA256 13f4e5782feb1e4f0623713dc81eb85359cad5f7dbb6f2b1ef6d16ae4dc44b49
MD5 107e7ae9c9fe5962083d7ce74020a03f
BLAKE2b-256 5a62f3a72a3d370a6925b7839f1841d17d089ad0a2cc60ad5159b96e08e7cea6

See more details on using hashes here.

Provenance

The following attestation bundles were made for lean_runtime-2.0.3-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

This release

2.0.3 This release

2 files

2.0.2

2 files

2.0.1

2 files

2.0.0

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