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:

Find the Lean project root (walks up to lakefile.lean / lakefile.toml)
Zip the project (excluding build artifacts)
Upload to the API and poll for completion
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

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

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

alephprover-0.2.3.tar.gz (11.1 kB view details)

Uploaded May 19, 2026 Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

The dropdown lists show the available interpreters, ABIs, and platforms. Enable javascript to be able to filter the list of wheel files.

alephprover-0.2.3-py3-none-any.whl (11.7 kB view details)

Uploaded May 19, 2026 Python 3

File details

Details for the file alephprover-0.2.3.tar.gz.

File metadata

Download URL: alephprover-0.2.3.tar.gz
Upload date: May 19, 2026
Size: 11.1 kB
Tags: Source
Uploaded using Trusted Publishing? Yes
Uploaded via: twine/6.1.0 CPython/3.13.12

File hashes

Hashes for alephprover-0.2.3.tar.gz
Algorithm	Hash digest
SHA256	`007bdfbd4cec2297af23e0894cc8696beb4888e01eae45e20ea41daf1a67a6e6`
MD5	`fd24162588314bc8b2e4a7bbc51a8ed6`
BLAKE2b-256	`f2593666cecc06c1f1576a57a4f3139e01fe55aa84f4427351855b42953b3cdd`

See more details on using hashes here.

Provenance

The following attestation bundles were made for alephprover-0.2.3.tar.gz:

Publisher: publish.yml on logiq-ai/alephprover

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Statement:
- Statement type: https://in-toto.io/Statement/v1
- Predicate type: https://docs.pypi.org/attestations/publish/v1
- Subject name: alephprover-0.2.3.tar.gz
- Subject digest: 007bdfbd4cec2297af23e0894cc8696beb4888e01eae45e20ea41daf1a67a6e6
- Sigstore transparency entry: 1573584220
- Sigstore integration time: May 19, 2026
Source repository:
- Permalink: logiq-ai/alephprover@75c5f41fa6d41a37e7410e3bb71386b5ca266ef5
- Branch / Tag: refs/tags/v0.2.3
- Owner: https://github.com/logiq-ai
- Access: internal
Publication detail:
- Token Issuer: https://token.actions.githubusercontent.com
- Runner Environment: github-hosted
- Publication workflow: publish.yml@75c5f41fa6d41a37e7410e3bb71386b5ca266ef5
- Trigger Event: push