LeanWarp

[LeanWarp by Isagoge Labs]

LeanWarp is hosted Lean 4 for formal verification. It checks and verifies proofs on workers that stay warm between edits, against a Lean release and the libraries your project pins. This SDK is how you and your agents use it: the leanwarp command, an MCP server and a Python library.

Get started · Agent setup · Reference · HTTP API · Documentation · Website

What it does

The reference lists every command and option; leanwarp skill --reference prints it.

Coming soon

These are planned and not available yet:

• Proof simplification: replace a proof with a shorter one that still checks.
• have extraction: lift named have blocks into top-level lemmas.
• Batch repair: fill several holes in one operation.

Install in two steps

1. Install. In a terminal, with uv:

uv tool install leanwarp && leanwarp setup

This installs the leanwarp command and its MCP server from PyPI. leanwarp setup adds the LeanWarp skill and MCP server to Claude Code, Codex and Cursor where they are installed, and the skill to ~/.agents/skills. It runs on Linux, macOS and WSL. You don't need Lean installed: LeanWarp runs Lean and Mathlib for you.

Or paste this into your agent:

Install LeanWarp: run uv tool install leanwarp && leanwarp setup, then ask me to sign in.

Already have LeanWarp 0.2 from GitHub? Its leanwarp-sdk tool owns the leanwarp command, so replace it instead:

uv tool uninstall leanwarp-sdk && uv tool install leanwarp && leanwarp setup

2. Sign in, in your own terminal:

leanwarp auth login

It opens the dashboard to create an API key; paste the key at the hidden prompt. Never paste it into an agent conversation. Then restart your agent.

When a new release is out, results include update_available; run leanwarp update to upgrade and refresh the installed skills.

Quick start

From your Lean project or one of the examples:

leanwarp doctor              # which environment this project runs onleanwarp connect             # create the project's workspaceleanwarp check LeanWarpExample.lean

If a command returns success: null (exit 3), run leanwarp wait until it finishes before submitting another operation. Then verify:

leanwarp verify LeanWarpExample.lean \  --declaration add_zero_example --target '∀ n : Nat, n + 0 = n'

Wait for that operation to finish too, then run leanwarp stop when you are done.

Every command prints one JSON object. Results start with success: true when the check passed or the proof was verified, false when it did not, and null while the work is still running, in which case run leanwarp wait. The exit code says the same thing: 0 passed, 1 did not pass, 2 the command failed, 3 still running.

Use with an agent

Give your agent the project directory and this instruction:

Run leanwarp skill and follow it. Use LeanWarp to check this Lean project and verify proofs against their intended statements. Reuse the workspace while you edit, and run leanwarp stop when you are done.

For MCP clients, add the server leanwarp --project /absolute/path/to/project mcp, or uvx leanwarp --project /absolute/path/to/project mcp without installing. It uses the same key and project state as the CLI. See agent setup. Keep API keys out of prompts, source files and tool arguments.

Your project and its environment

LeanWarp uploads only your .lean files. Lean, Mathlib and every other dependency come from an environment: a Lean release with pinned libraries, already built on LeanWarp's workers. Run leanwarp environments to list them. leanwarp files lists what would upload; patterns in .gitignore and .leanwarpignore leave files out.

leanwarp connect picks the environment for you:

• If your project's lean-toolchain and lake-manifest.json match an environment, it uses that one, so results agree with your local build.
• If your project has neither file, as with a folder of .lean files, it uses the only served environment, or the newest served stable Lean release when there are several.
• If they match no environment, it stops and lists the ones available. Run leanwarp connect --environment NAME to check your files there anyway; they then compile against that environment's Lean and Mathlib.

To start a new project, copy one of the examples, which match the environments LeanWarp serves.

Lean versions and libraries

The LeanWarp engine supports every stable Lean 4 release from 4.26.0, with the Lake libraries a project locks. The hosted service runs it in the environments listed on the website, which today pair Lean with Mathlib. Each one is built and tested before it is served, so your first check starts from compiled libraries. If your project needs another Lean release or library, open an issue with its lean-toolchain and lake-manifest.json.

Billing

You pay from prepaid credit, billed by the second while a worker runs. Run leanwarp resources to see the published worker's starting minute price, whether charges depend on usage, startup credit hold and idle timeout. LeanWarp selects the worker. Use leanwarp connect --max-spend 2 to create a workspace with a $2 cap, or edit an existing cap in the dashboard. Reconnecting without a cap keeps the saved cap.

When the worker uses usage billing, CPU and RAM charges increase independently above their reserved baselines. The starting rate is a paid minimum while the worker runs, including idle time. Bursting depends on available host capacity. Otherwise, the listed minute rate applies for the time the worker runs. Existing workspaces keep their saved billing terms.

A worker starts with your first operation and stays warm between calls. Run leanwarp stop when finished; closing the SDK client or your terminal does not stop it. Unused held credit is released once shutdown and final usage are confirmed. Stopping keeps your uploaded files and completed results; the next operation reconstructs the worker. Set a spending cap for each workspace in the dashboard.

Concepts

Documentation

The agent instructions ship with the package: leanwarp skill prints the workflow and leanwarp skill --reference the full reference. Run leanwarp --help or leanwarp COMMAND --help for arguments.