Lean 4 Proof Checker
Pricing
$50.00 / 1,000 proof checks
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.
You can access the Lean 4 Proof Checker programmatically from your own applications by using the Apify API. You can also choose the language preference from below. To use the Apify API, you’ll need an Apify account and your API token, found in API & Integrations in Apify Console.
$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-datasetThe Apify CLI is the official tool that allows you to use Lean 4 Proof Checker locally, providing convenience functions and automatic retries on errors.
Using installation script (macOS/Linux):
$curl -fsSL https://apify.com/install-cli.sh | bashUsing installation script (Windows):
$irm https://apify.com/install-cli.ps1 | iexUsing Homebrew:
$brew install apify-cliUsing npm:
$npm install -g apify-cliOther API clients include: