Lean 4 Proof Checker
Pricing
Pay per event
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.
Pricing
Pay per event
Rating
0.0
(0)
Developer
D. Michael Piscitelli
Maintained by CommunityActor stats
1
Bookmarked
2
Total users
1
Monthly active users
19 days ago
Last modified
Categories
Share
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: