Aleph Prover CLI

Prove Lean4 theorems with the Aleph Prover API from your terminal or from Claude Code.

Install

# Run directly with uvx (no install needed)
uvx alephprover prove <file_path> <theorem_name>

# Or install globally
uv tool install alephprover

# Or with pip
pip install alephprover

Usage

# Set your API key (get one at https://alephprover.logicalintelligence.com/account)
export PROVER_API_KEY="sk-aleph-..."

# Submit a proof request
alephprover prove Mathlib/Algebra/Group/Basic.lean mul_left_cancel

# With hints and budgets
alephprover prove MyProject/Basic.lean my_theorem \
  --hints "try induction on n" \
  --time-budget 30 \
  --cost-budget 10

The CLI will:

1. Find the Lean project root (walks up to lakefile.lean / lakefile.toml)
2. Zip the project (excluding build artifacts)
3. Upload to the API and poll for completion
4. Download and apply the proof diff via git apply

Other commands

# Check request status
alephprover status <request_id>

# List your proof requests
alephprover list
alephprover list --search "mul_left_cancel"

# Continue a partial or cancelled request with new budget
alephprover continue <request_id>
alephprover continue <request_id> --time-budget 60 --cost-budget 20 --hints "try simp first"

# Cancel a running request
alephprover cancel <request_id>

# Download results or specific artifacts
alephprover download <request_id>
alephprover download <request_id> --artifact <artifact_id> -o output.zip

Claude Code Skill

Install the /prove skill for Claude Code:

# Install in current project
uvx alephprover install-skill

# Or install globally (available in all projects)
uvx alephprover install-skill --global

Then in Claude Code:

/prove mul_left_cancel in Mathlib/Algebra/Group/Basic.lean
/prove my_theorem in MyProject/Basic.lean with hint: try induction on n

Configuration

Requirements

• Python >= 3.10
• uv (for uvx usage) or pip install alephprover
• git (for applying patches)
• An Aleph Prover account with an API key