alephprover 0.1.0

CLI tool for submitting Lean proof requests to the Aleph Prover API

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

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

Variable	Required	Default	Description
PROVER_API_KEY	Yes	—	API key (sk-aleph-...) from Account Settings
PROVER_API_URL	No	https://alephprover.logicalintelligence.com	API base URL

Requirements

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