Documentation

Note: API access is currently limited to select accounts. If you don't see the API Keys section in your Account Settings, your account does not have API access yet.

Getting Started

Aleph Prover automatically proves Lean 4 theorems. You can submit proof requests through the web interface, the CLI tool, or directly from Claude Code.

1. Get an API Key

1. Go to Account Settings → API Keys
2. Click Create New Key
3. Copy the key immediately — it is only shown once

Your API key starts with sk-aleph-. Set it as an environment variable:

export PROVER_API_KEY="sk-aleph-..."

To persist it, add the line above to your shell profile (~/.bashrc, ~/.zshrc, etc.).

2. CLI Tool

The alephprover CLI submits proof requests from your terminal and applies the result automatically.

uvx alephprover prove Mathlib/Algebra/Group/Basic.lean mul_left_cancel

See the full documentation on PyPI for installation options, configuration, and all CLI flags.

3. Claude Code Skill

Use Aleph Prover directly from Claude Code with the /prove skill.

uvx alephprover install-skill

Then in Claude Code:

/prove mul_left_cancel in Mathlib/Algebra/Group/Basic.lean

See the full documentation on PyPI for more details.

4. API Reference

For direct API integration, see the interactive API documentation.