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 or resolves the environment, checks a global OCI cache, and returns structured Lean results with exact provenance.

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 diff 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.

Under the hood

The simple API is backed by exact Git commits and trees, Lake-resolved locks, platform-aware content-addressed environments, atomic cross-process builds, transparent OCI cache reuse, replayable provenance, verification, and signed attestations. Advanced users can access all of it through lean_runtime.Runtime and the lean-runtime operations CLI.

Documentation

License

Apache License 2.0.

Project links

Data verified by PyPI on Aug 4, 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 4, 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-1.0.0.tar.gz (132.2 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-1.0.0-py3-none-any.whl (101.5 kB view details)

Uploaded Python 3

File details

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

File metadata

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

File hashes

Hashes for lean_runtime-1.0.0.tar.gz
Algorithm Hash digest
SHA256 98014532c3730df516db9a328d1ddda1716bb3e2a24e008bfa9ebb615bb1f8da
MD5 5101e849fda3d966abf7078c47773b27
BLAKE2b-256 d117cda729101e91fb28a88d735cb0271124ca835a3aabdeac95cf50cfa376aa

See more details on using hashes here.

Provenance

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

File metadata

  • Download URL: lean_runtime-1.0.0-py3-none-any.whl
  • Upload date:
  • Size: 101.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-1.0.0-py3-none-any.whl
Algorithm Hash digest
SHA256 fb36fc3e64f7e518ed8d1c3c579beabd0db7e095b5bc20b6058aa214240dee79
MD5 73f8301b1bed5155d3c9bf455861adbf
BLAKE2b-256 88b088193ccdc5ca46d1eb31eb767ac272e38953d724194a6fdee2f29948b9af

See more details on using hashes here.

Provenance

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

2.0.0

2 files

This release

1.0.0 This release

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