Lean Runtime
Check the proof. Reuse everything else.
python -m pip install lean-runtime
Give Lean Runtime an ordinary file:
-- Main.lean
import Mathlib.Tactic.NormNum
example : 2 + 2 = 4 := by norm_num
$ lean-runtime check Main.lean
No Lake project, dependency checkout, or toolchain setup required. Lean Runtime discovers and verifies the exact environment, then keeps it ready for offline reuse.
Get started · Read the documentation · Explore the CLI
The model
| Noun | Meaning |
|---|---|
| context | where a file's requirements come from: --using, frontmatter, the owning Lake project, or automatic discovery |
| environment | one exact, immutable toolchain + package set |
| lock | an environment written down, reusable offline anywhere |
| verdict | Lean's answer inside one environment: accepted or rejected |
Discovery proposes an environment. Only Lean accepts it. lean-runtime status
shows the proposal without running anything; lean-runtime check produces the
verdict and names the environment it was produced in:
✓ Main.lean accepted in mathlib-v4.33.0 (3.21s)
Start where you are
Create a project:
lean-runtime new MyProof
cd MyProof
lean-runtime check
lean-runtime build
Use an existing pinned Lake project from its directory:
lean-runtime check
lean-runtime adopt
adopt verifies the existing exact dependency graph, previews reuse and disk
recovery, asks for confirmation, and swaps dependency links atomically. It does
not change lean-toolchain or lake-manifest.json. Passing a directory that
contains several projects discovers them automatically:
lean-runtime adopt ~/research
Check a standalone source file:
lean-runtime check Main.lean
The same command uses the nearest pinned Lake project when one exists and
otherwise performs bounded exact-environment discovery. Automatic discovery
uses retained or verified downloadable environments; building a missing
candidate from source requires --allow-source-build.
Record the environment only when the result must be reproduced elsewhere:
lean-runtime check Main.lean --write-lock environment.lock.json
A file can instead name its environment in strict comment frontmatter:
-- /// lean-runtime
-- requires = ["mathlib@v4.33.0"]
-- ///
import Mathlib
example : 2 + 2 = 4 := by norm_num
When discovery needs an override, there is one spelling:
lean-runtime check Main.lean --using mathlib@v4.33.0
lean-runtime check Main.lean --using environment.lock.json
lean-runtime check Main.lean --using research-stack
lean-runtime check Main.lean --using lean:v4.33.0
lean-runtime check Main.lean --using ~/proofs/MyProject
Typed package:, lock:, env:, toolchain:, and project: prefixes resolve
rare ambiguities. A project context applies to files inside that project's
root. Persistent store, registry, and trust policy belongs in
environment configuration rather than everyday command lines.
Commands
The normal surface is deliberately small:
new NAME create a project
adopt [PATH] share dependencies from existing project(s)
check [PATH…] check a project, directory, source file, or stdin (-)
watch FILE re-check on save
build [TARGET] build the current project
update preview and apply a safe project update
publish configure verified project publication
status [PATH] dry run of check: where the environment comes from, what it costs
verify SUBJECT verify an exact artifact
doctor diagnose and offer safe repairs
clean preview and reclaim unused storage
replay CAPTURE replay an execution capture
completion SHELL generate shell completion
Project commands use the current directory when no path is supplied. Every
command that changes a project, deletes local content, or publishes to a remote
shows its plan and asks before changing anything; automation passes --yes,
and inspection-only calls pass --dry-run.
Persistent registry, availability, store, and publisher-trust policy belongs
in ~/.config/lean-runtime/config.toml; the nearest project's
lean-runtime.toml can override it. Daily commands therefore normally need no
configuration flags.
Exact and operator workflows live under noun namespaces:
env list · info · lock · acquire · diff · export · import
project info · scan · share · unshare · lock · export
program create · run · info · acquire · export · import · publish
toolchain list · info · install · optimize
storage usage · verify
catalog catalog maintenance
There are no v3 command aliases. run, init, prepare, open, download,
environments, inspect, compare, copy, finalize, lean-run, and
lean-runtime-catalog were removed in 4.0.
Existing Elan installations
Lean Runtime automatically reuses an exact compatible toolchain already
installed by the user's Elan. This access is read-only: it never changes the
user's default, installs into the user's Elan home, or removes user toolchains.
Missing toolchains and downloadable slim checking runtimes remain isolated in
Lean Runtime's private store. lean-runtime status and doctor expose the
choice when it matters.
Exact environments
lean-runtime env lock environment.toml --output environment.lock.json
lean-runtime env acquire environment.lock.json --name research-stack
lean-runtime env info research-stack
lean-runtime env diff previous.lock.json environment.lock.json
lean-runtime env export research-stack --output research-stack.lean-environment
lean-runtime env import research-stack.lean-environment --name imported-stack
Locks are canonical and content-addressed. Full environments preserve source; downloaded sparse capsules project only verified import closures and keep the same environment identity as their projection grows.
Python
import lean_runtime as lean
env = lean.setup(deps=["mathlib@v4.33.0"])
result = env.check("import Mathlib\nexample : 2 + 2 = 4 := by norm_num\n")
result.raise_for_error()
The Python API retains the explicit Runtime, EnvironmentSpec,
EnvironmentLock, project, capture, program, cancellation, and verification
interfaces for infrastructure code.
Guarantees and limits
- Exact Git commits, trees, locks, toolchains, platform identities, and artifact digests are verified before an environment becomes ready.
- Acquisitions and project sharing are staged, probed, and published atomically.
- User project metadata and user Elan state are not silently rewritten.
- The local execution backend enforces supported resource limits but is not a network sandbox; unsupported isolation requests fail explicitly.
- A Lean rejection is a normal verdict and exits 1. Invalid or infrastructure invocations exit 2 and carry no verdict. Publication failures retain their documented classified exit statuses.
Documentation lives at alerad.github.io/lean-runtime.
1 maintainer
Metadata
1 maintainer
Release files for lean-runtime 4.33.0.1
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | Provenance | |
|---|---|---|---|---|
| lean_runtime-4.33.0.1.tar.gz | 952.2 kB | With provenance | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| lean_runtime-4.33.0.1-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 1.8 MB
Release files / lean_runtime-4.33.0.1.tar.gz
| Download URL | lean_runtime-4.33.0.1.tar.gz |
|---|---|
| Size | 952.2 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
24c54fc668e121db8b49aabb41d624d25fbfb7fb19a4d50d39e15a2d75f2db72
|
|
BLAKE2b-256 checksum How to use checksums |
99bdbbcd4855b1d4ec3bf935f40c238fadf3f3fdf0d1c9ada3a5d06fabaef867
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Sep 14, 2026.
Transparency logRelease files / lean_runtime-4.33.0.1-py3-none-any.whl
| Download URL | lean_runtime-4.33.0.1-py3-none-any.whl |
|---|---|
| Size | 822.6 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
5ff0205f179eb3eb1f31ddd321b1ae99ac245e55663d94ee4ae264ef5b13b39d
|
|
BLAKE2b-256 checksum How to use checksums |
487360f0789f31ce8ea5fd4f4fccb67a7c6c390bb04f8a0a319af27dae0932e7
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/7.0.0 CPython/3.13.14
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Sep 14, 2026.
Transparency logSecurity for lean-runtime 4.33.0.1
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
Full provenance
All 2 files in this release have been uploaded with provenance metadata.
Attestation for lean_runtime-4.33.0.1.tar.gz
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Sep 14, 2026.
Transparency logA note on package security
PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.
