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 6, 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 6, 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.2.tar.gz (145.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.2-py3-none-any.whl (112.2 kB view details)

Uploaded Python 3

File details

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

File metadata

  • Download URL: lean_runtime-2.0.2.tar.gz
  • Upload date:
  • Size: 145.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.2.tar.gz
Algorithm Hash digest
SHA256 1ee8b3470d6a673c942d7785dd3db4d57680db19c5d77e12c906a0b5d56a1742
MD5 3d6cb571b39910b6367af8cba5172a1c
BLAKE2b-256 ccae42808e2330dd07359c80e58bb9086409503a2193726b25b9f66d8a7a9f4b

See more details on using hashes here.

Provenance

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

File metadata

  • Download URL: lean_runtime-2.0.2-py3-none-any.whl
  • Upload date:
  • Size: 112.2 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.2-py3-none-any.whl
Algorithm Hash digest
SHA256 3e89102f80e116e22ca562538de1c023da6b0109abe89d8d4d3abe62eef674d2
MD5 db2c9f25e791c5c68b7453ed8442c66d
BLAKE2b-256 ba5ff7d7d20d316afa85690357658eab2dfe10337f36b09ebfbee6fddd6bcc10

See more details on using hashes here.

Provenance

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

This release

2.0.2 This release

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