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.
1import { ApifyClient } from 'apify-client';2
3// Initialize the ApifyClient with your Apify API token4// Replace the '<YOUR_API_TOKEN>' with your token5const client = new ApifyClient({6 token: '<YOUR_API_TOKEN>',7});8
9// Prepare Actor input10const input = {11 "proofs": [12 {13 "source": "namespace Canary\ntheorem add_comm' (a b : Nat) : a + b = b + a := Nat.add_comm a b\nend Canary\n",14 "theorem": "Canary.add_comm'"15 }16 ]17};18
19// Run the Actor and wait for it to finish20const run = await client.actor("herakles-dev/lean-proof-check").call(input);21
22// Fetch and print Actor results from the run's dataset (if any)23console.log('Results from dataset');24console.log(`💾 Check your data here: https://console.apify.com/storage/datasets/${run.defaultDatasetId}`);25const { items } = await client.dataset(run.defaultDatasetId).listItems();26items.forEach((item) => {27 console.dir(item);28});29
30// 📚 Want to learn more 📖? Go to → https://docs.apify.com/api/client/js/docsThe Apify API client for JavaScript is the official library that allows you to use Lean 4 Proof Checker API in JavaScript or TypeScript, providing convenience functions and automatic retries on errors.
Install the apify-client
$npm install apify-clientOther API clients include: