Build Lean Server from Source

This guide walks you through setting up the Lean Server from source code, providing a high-performance REST API for executing and verifying Lean 4 mathematical proofs.

Prerequisites

Before starting, ensure you have the following installed on your system:

• uv or Conda: We strongly recommend using uv. You can follow this link for installation.
• elan: You can follow this tutorial to install elan.

Installation Steps

1. Clone the Repository

Choose your preferred method to clone the repository:

# Clone using HTTPS
git clone https://github.com/EvolvingLMMs-Lab/lean-runner.git
cd lean-runner

2. Set Up Python Environment

Create and activate a Python virtual environment with the required Python version:

# Create virtual environment with Python 3.12
uv venv --python=3.12

# Activate the virtual environment
source .venv/bin/activate

# Create virtual environment with Python 3.12
uv venv --python=3.12

# Activate the virtual environment
.venv\Scripts\activate

# Create a new conda environment with Python 3.12
conda create -n lean-server python=3.12
conda activate lean-server

3. Install Server Package

Install the server package in editable mode to enable development:

# Install the server package with all dependencies
uv pip install -e packages/server

# Install the server package with all dependencies
python -m pip install -e packages/server

4. Build Lean Dependencies

Build the Lean workspace and install required mathematical libraries:

# Navigate to the Lean playground
cd playground

# Build all Lean dependencies (this may take several minutes)
lake build

# Return to the project root
cd ..

Running the Server

Basic Server Startup

Start the server with default settings:

# Ensure virtual environment is activated
source .venv/bin/activate

# Start the server
lean-server --port=8888 --concurrency=32

Command Line Options

The lean-server command supports the following options:

lean-server --host=127.0.0.1 --port=8000 --reload --log-level=DEBUG

lean-server --host=0.0.0.0 --port=8000 --concurrency=32--log-level=INFO

lean-server --host=0.0.0.0 --port=8000 --concurrency=128 --log-level=WARNING

Verify Installation

Test that the server is working correctly:

1. Check Server Status

# In one terminal, start the server
lean-server --host=0.0.0.0 --port=8000

# In another terminal, test the health endpoint
curl http://localhost:8000/health

# Open your web browser and navigate to:
http://localhost:8000/health

# You should see a JSON response in the browser

import requests

response = requests.get("http://localhost:8000/health")
print(response.json())

Expected response:

{"status": "ok", "message": "Lean Server is running", "version": "0.0.1"}

2. Test Proof Verification

curl -X POST http://localhost:2333/prove/check \
  -F "proof=import Mathlib.Tactic.NormNum
      theorem test : 2 + 2 = 4 := by norm_num"

{"success":true,"status":"finished","result":{"env":0,"messages":[]},"error_message":null}

from lean_runner import LeanClient

proof = """\
import Mathlib.Tactic.NormNum

theorem test : 1 + 1 = 2 := by norm_num
"""

with LeanClient(base_url="http://localhost:8000") as client:
    result = client.verify(proof=proof)
    print(result.model_dump_json(indent=4))

{
    "success": true,
    "status": "finished",
    "result": {
        "env": 0,
        "messages": []
    },
    "error_message": null
}

Next Steps

After successful installation:

1. Read the Client Documentation to learn how to interact with the server
2. Explore the API Documentation for detailed endpoint reference