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:

{
  "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):

{
  "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.