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.
# Set API token$API_TOKEN=<YOUR_API_TOKEN>
# Prepare Actor input$cat > input.json << 'EOF'<{< "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'"< }< ]<}<EOF
# Run the Actor using an HTTP API# See the full API reference at https://docs.apify.com/api/v2$curl "https://api.apify.com/v2/actors/herakles-dev~lean-proof-check/runs?token=$API_TOKEN" \< -X POST \< -d @input.json \< -H 'Content-Type: application/json'Below, you can find a list of relevant HTTP API endpoints for calling the Lean 4 Proof Checker Actor. For this, you’ll need an Apify account. Replace <YOUR_API_TOKEN> in the URLs with your Apify API token, which you can find under API & Integrations in Apify Console. For details, see the API reference.
https://api.apify.com/v2/actors/herakles-dev~lean-proof-check/runs?token=<YOUR_API_TOKEN>Note: By adding the method=POST query parameter, this API endpoint can be called using a GET request and thus used in third-party webhooks. Please refer to our Run Actor API documentation.
https://api.apify.com/v2/actors/herakles-dev~lean-proof-check/run-sync-get-dataset-items?token=<YOUR_API_TOKEN>Note: This endpoint supports both POST and GET request methods. However, only the POST method allows you to pass input data. For more information, please refer to our Run Actor synchronously and get dataset items API documentation.
https://api.apify.com/v2/actors/herakles-dev~lean-proof-check?token=<YOUR_API_TOKEN>For more information, please refer to our Get Actor API documentation.
Actors can be used to scrape web pages, extract data, or automate browser tasks. Use the Lean 4 Proof Checker API programmatically via the Apify API.
You can choose from:
You can start Lean 4 Proof Checker with the Apify API by sending an HTTP POST request to the Run Actorendpoint. An Actor’s input and its content type can be passed as a payload of the POST request, and additional options can be specified using URL query parameters. The Lean 4 Proof Checker is identified within the API by its ID, which is the creator’s username and the name of the Actor.
When the Lean 4 Proof Checker run finishes you can list the data from its default dataset(storage) via the API or you can preview the data directly on Apify Console.