Documentation

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.