# Lean 4 Proof Checker (`herakles-dev/lean-proof-check`) Actor

Checks a Lean 4 proof with Lean's own kernel and says whether the named theorem is proved, with no sorry and no extra axioms. Core Lean (Init and Std), no Mathlib. For AI agents that write proofs.

- **URL**: https://apify.com/herakles-dev/lean-proof-check.md
- **Developed by:** [D. Michael Piscitelli](https://apify.com/herakles-dev) (community)
- **Stats:** 2 total users, 1 monthly users, 100.0% runs succeeded, 0 bookmarks
- **User rating**: No ratings yet

## Pricing

$50.00 / 1,000 proof checks

This Actor is paid per event. You are not charged for the Apify platform usage, but only a fixed price for specific events.

Learn more: https://docs.apify.com/actors/running/actors-in-store.md#pay-per-event

## What's an Apify Actor?

An Actor is a serverless cloud program that runs on the Apify platform. It has two run modes.
In Batch mode, an Actor accepts a well-defined JSON input, performs an action which can take anything from a few seconds to a few hours,
and optionally produces a well-defined JSON output, datasets with results, or files in key-value store.
In Standby mode, an Actor provides a web server which can be used as a website, API, or an MCP server.

Apify vocabulary and the platform model are defined once, in the agent quickstart at https://apify.com/agents.md.

## How to integrate an Actor?

If asked about integration, you help developers integrate Actors into their projects.
You adapt to their stack and deliver integrations that are safe, well-documented, and production-ready.

Do not guess an integration path. Every one of them is in the agent quickstart at https://apify.com/agents.md: the Apify MCP server, Agent Skills with the Apify CLI, the JavaScript and Python clients, the REST API, and the account-free path for an agent with no human to sign in. It also carries the rule on stating cost before the first paid run.

For examples already wired to this Actor's own input schema, see the [API](#api) section below.

Each client library has reference documentation the quickstart does not restate: [JavaScript/TypeScript](https://docs.apify.com/api/client/js/docs.md) (`npm install apify-client`) and [Python](https://docs.apify.com/api/client/python/docs.md) (`pip install apify-client`).

# README

## Lean 4 Proof Checker

Checks a Lean 4 proof with Lean's own kernel and says whether the named theorem is proved, with no sorry and no extra axioms. Core Lean (Init and Std), no Mathlib. For AI agents that write proofs.

### What it does

Send a Lean 4 file and the name of a theorem in it, and Lean's own kernel checks the proof. You get back verified or failed, the axioms the proof depends on, whether it uses `sorry`, the statement Lean says was proved, and Lean's error messages with line numbers. It's for AI agents that write proofs and need an answer they can act on without installing Lean.

### For AI agents

Call it with one JSON object and read one dataset row per entry. Every row has the same fields, so an agent can rely on them:

- `input_index`: the entry's position in your input list, starting at 0. Rows come back in input order, and this lets you match each row to its entry without comparing text.
- `outcome`: `ok`, `empty` (nothing found, not charged), `out_of_scope` (refused, not charged), `error` (not charged) or `skipped` (a limit was reached, not charged).
- `units_charged`: how many proof-check events this entry cost you.
- `result`: the typed result for `ok` rows, `null` otherwise.
- `error`: `{type, message, retryable}` when something went wrong, `null` otherwise. `type` is a fixed list of codes, and `retryable` says whether the same entry may succeed on a later run.

Example input:

```json
{
  "proofs": [
    {
      "source": "namespace Canary\ntheorem add_comm' (a b : Nat) : a + b = b + a := Nat.add_comm a b\nend Canary\n",
      "theorem": "Canary.add_comm'"
    }
  ]
}
```

One real row from a platform test run (build 0.1.1):

```json
{
  "input_index": 2,
  "source": "Pyr.z",
  "outcome": "ok",
  "units_charged": 1,
  "result": {
    "verdict": "verified",
    "theorem": "Pyr.z",
    "statement": "Pyr.z : ∀ (n : Nat), 0 + n = n",
    "axioms": [],
    "disallowed_axioms": [],
    "uses_sorry": false,
    "errors": [],
    "reason": "Lean's kernel accepted the proof, using only the standard axioms.",
    "elapsed_s": 0.805,
    "lean_version": "4.33.1"
  },
  "notices": [],
  "error": null,
  "cost_usd": 0,
  "latency_s": 1.467
}
```

### Input

- `proofs`: Each entry is one Lean 4 source file and the full name of the theorem in it to check. Up to 10 entries per run, each up to 21000 characters.
  Each entry is a JSON object with these fields:
  - `source` (string, required): Lean 4 source. A whole Lean 4 file. Imports may only name Init or Std modules (core Lean, no Mathlib). No #commands, macros, syntax, set\_option or code that runs while checking.
  - `theorem` (string, required): Theorem name. The full name of the theorem to check, declared in the source, for example MyProofs.add\_comm.

### Output

One dataset row per entry, in input order. The Overview tab shows the same rows as a table.

### Pricing

$0.05 per proof check. You pay only for entries it actually delivered. Empty results, refused entries, errors and skipped entries are never charged. Runs on the free Apify plan handle up to 3 per run.

### Limits

- Up to 10 entries per run.

- Each entry up to 21000 characters.

- Time limit per entry: 45 s. An entry that runs longer is stopped, returned as a `timeout` error and not charged.

- Typical time per entry: about 1 s (p50 1.1 s, p95 4.8 s on the platform), plus about 9 s to start a run.

- Core Lean only: imports may name Init or Std. Mathlib and other packages aren't available.

- It checks proofs; it doesn't write or repair them.

- It never runs code from your file. `#eval`, macros, `set_option`, `native_decide` and similar are refused anywhere in the file, comments and strings included, and a refused entry isn't charged.

- A private theorem, or a name Init or Std already has, can't be checked.

### Contact

Questions or a wrong result: open an issue on the Actor's Issues tab. I read them and reply within two business days.

# Actor input Schema

## `proofs` (type: `array`):

Each entry is one Lean 4 source file and the full name of the theorem in it to check.

## Actor input object example

```json
{
  "proofs": [
    {
      "source": "namespace Canary\ntheorem add_comm' (a b : Nat) : a + b = b + a := Nat.add_comm a b\nend Canary\n",
      "theorem": "Canary.add_comm'"
    }
  ]
}
```

# Actor output Schema

## `results` (type: `string`):

One dataset item per input entry: its outcome (ok, empty, out\_of\_scope, error, skipped), units charged, the typed result, notices and any error.

## `overview` (type: `string`):

The same items as a table: one row per entry with its outcome and charge.

# API

You can run this Actor programmatically using our API. Below are code examples in JavaScript, Python, and CLI, as well as the OpenAPI specification and MCP server setup.

## JavaScript example

```javascript
import { ApifyClient } from 'apify-client';

// Initialize the ApifyClient with your Apify API token
// Replace the '<YOUR_API_TOKEN>' with your token
const client = new ApifyClient({
    token: '<YOUR_API_TOKEN>',
});

// Prepare Actor input
const input = {
    "proofs": [
        {
            "source": "namespace Canary\ntheorem add_comm' (a b : Nat) : a + b = b + a := Nat.add_comm a b\nend Canary\n",
            "theorem": "Canary.add_comm'"
        }
    ]
};

// Run the Actor and wait for it to finish
const run = await client.actor("herakles-dev/lean-proof-check").call(input);

// Fetch and print Actor results from the run's dataset (if any)
console.log('Results from dataset');
console.log(`💾 Check your data here: https://console.apify.com/storage/datasets/${run.defaultDatasetId}`);
const { items } = await client.dataset(run.defaultDatasetId).listItems();
items.forEach((item) => {
    console.dir(item);
});

// 📚 Want to learn more 📖? Go to → https://docs.apify.com/api/client/js/docs

```

## Python example

```python
from apify_client import ApifyClient

# Initialize the ApifyClient with your Apify API token
# Replace '<YOUR_API_TOKEN>' with your token.
client = ApifyClient("<YOUR_API_TOKEN>")

# Prepare the Actor input
run_input = { "proofs": [{
            "source": """namespace Canary
theorem add_comm' (a b : Nat) : a + b = b + a := Nat.add_comm a b
end Canary
""",
            "theorem": "Canary.add_comm'",
        }] }

# Run the Actor and wait for it to finish
run = client.actor("herakles-dev/lean-proof-check").call(run_input=run_input)

# Fetch and print Actor results from the run's dataset (if there are any)
print(f"💾 Check your data here: https://console.apify.com/storage/datasets/{run.default_dataset_id}")
for item in client.dataset(run.default_dataset_id).iterate_items():
    print(item)

# 📚 Want to learn more 📖? Go to → https://docs.apify.com/api/client/python/docs/quick-start

```

## CLI example

```bash
echo '{
  "proofs": [
    {
      "source": "namespace Canary\\ntheorem add_comm'\'' (a b : Nat) : a + b = b + a := Nat.add_comm a b\\nend Canary\\n",
      "theorem": "Canary.add_comm'\''"
    }
  ]
}' |
apify call herakles-dev/lean-proof-check --silent --output-dataset

```

## MCP server setup

```json
{
    "mcpServers": {
        "apify": {
            "type": "http",
            "url": "https://mcp.apify.com/?tools=fetch-actor-details,herakles-dev/lean-proof-check"
        }
    }
}
```

The hosted server signs you in with OAuth on first connect, so no API token belongs in this config. Clients without OAuth support can send an `Authorization: Bearer <APIFY_API_TOKEN>` header instead, using a token from API & Integrations in Apify Console (https://console.apify.com/settings/integrations).

## OpenAPI specification

Download the OpenAPI definition: https://api.apify.com/v2/actors/S95dCLnUohldHFhXl/builds/c7Gs38IPRbeu0KcyX/openapi.json