API Reference

This document provides a comprehensive reference for all RESTful API endpoints available in the Lean Prover Server.

Endpoints

Health Check

GET /health

Verifies the server's operational status and retrieves basic information.

Responses - 200 OK: Server is running. - 500 Internal ServerError: Server-side processing error.

Success Response 200 OK

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

cURL Example

curl "http://localhost:8000/health"

Proof Verification

POST /prove/check

Synchronously verifies a Lean proof for correctness.

Parameters

Responses - 200 OK: Verification finished. - 500 Internal Server Error: Server-side processing error.

Success Response 200 OK

{
  "success": true,
  "status": "finished",
  "result": { ... },
  "error_message": null
}

cURL Example

curl -X POST "http://localhost:8000/prove/check" \
  -H "Content-Type: application/x-www-form-urlencoded" \
  -d "proof=theorem test : 1 + 1 = 2 := by norm_num" \
  -d "config={}"

Python Example

import requests
import json

response = requests.post(
    "http://localhost:8000/prove/check",
    data={
        "proof": "theorem test : 1 + 1 = 2 := by norm_num",
        "config": json.dumps({
            "timeout": 600.0,
            "memory_limit_mb": 512
        })
    }
)
print(response.json())

POST /prove/submit

Submits a Lean proof for asynchronous processing and returns a unique proof_id.

Parameters

Responses - 200 OK: Proof submitted successfully. - 502 Bad Gateway: Error during proof submission.

Success Response 200 OK

{
  "proof_id": "your-unique-proof-id"
}

cURL Example

curl -X POST "http://localhost:8000/prove/submit" \
  -H "Content-Type: application/x-www-form-urlencoded" \
  -d "proof=theorem hard_proof : some_complex_statement := by sorry" \
  -d 'config={"timeout": 900.0}'

Python Example

import requests
import json

response = requests.post(
    "http://localhost:8000/prove/submit",
    data={
        "proof": "theorem complex_proof : some_statement := by tactic_sequence",
        "config": json.dumps({
            "timeout": 900.0,
            "memory_limit_mb": 2048
        })
    }
)
proof_id = response.json().get("proof_id")
print(f"Submitted proof with ID: {proof_id}")

GET /prove/result/{proof_id}

Retrieves the result of a previously submitted asynchronous proof.

Path Parameters

Responses - 200 OK: Result retrieved successfully. - 404 Not Found: The specified proof_id does not exist. - 500 Internal Server Error: Server-side processing error.

Success Response 200 OK

{
  "success": true,
  "status": "finished",
  "result": { ... },
  "error_message": null
}

cURL Example

curl "http://localhost:8000/prove/result/your-proof-id-here"

Python Example

import requests

proof_id = "your-proof-id-here"
response = requests.get(f"http://localhost:8000/prove/result/{proof_id}")
print(response.json())

Database Management

GET /db/fetch

Fetches records from the database using an SQL query and streams the results.

Query Parameters

Responses - 200 OK: Query executed successfully. - 500 Internal Server Error: Database error.

cURL Example

curl "http://localhost:8000/db/fetch?query=SELECT * FROM proof LIMIT 10&batch_size=5"

Python Example

import requests

response = requests.get(
    "http://localhost:8000/db/fetch",
    params={
        "query": "SELECT * FROM proof WHERE created_at > '2025-01-01'",
        "batch_size": 50
    },
    stream=True
)

for chunk in response.iter_content(chunk_size=1024):
    if chunk:
        print(chunk.decode('utf-8'))

DELETE /db/clean

Cleans the database by removing proof records older than a specified time.

Query Parameters

Responses - 200 OK: Database cleaned successfully. - 500 Internal Server Error: Database error.

Success Response 200 OK

{
  "message": "Database cleaned successfully"
}

cURL Example

# Clean records older than 1 hour (3600 seconds)
curl -X DELETE "http://localhost:8000/db/clean?seconds=3600"

Python Example

import requests

# Clean records older than 24 hours (86400 seconds)
response = requests.delete(
    "http://localhost:8000/db/clean",
    params={"seconds": 86400}
)
print(response.json())

Data Structures

Proof Configuration

The config parameter is a JSON string used to customize proof verification.

Default Configuration

{
  "timeout": 300.0,
  "all_tactics": false,
  "tactics": false,
  "ast": false,
  "premises": false,
  "memory_limit_mb": 8192
}

Options

Proof Result

The proof verification endpoints (/prove/check and /prove/result/{proof_id}) return a JSON object with the following structure.

Result Object

{
  "success": true,
  "status": "finished",
  "result": {
    "tactics": [],
    "ast": {},
    "premises": []
  },
  "error_message": null
}

Fields

Memory Limits

The server supports memory limits for Lean processes to prevent excessive resource consumption. When a process exceeds the memory limit:

1. The process is automatically terminated by the operating system
2. The server returns a specific error response with status: "memory_limit_exceeded"
3. The return_code will be -9 (SIGKILL signal)

Error Handling

API errors are returned in a consistent JSON format.

Error Response

{
  "detail": "A descriptive error message."
}

Memory Limit Error Response

{
  "success": false,
  "status": "error",
  "result": {
    "status": "memory_limit_exceeded",
    "return_code": -9
  },
  "error_message": "Process was killed due to memory limit (512 MB)"
}

Common Status Codes