Metadata-Version: 2.4
Name: alephprover
Version: 0.1.0
Summary: CLI tool for submitting Lean proof requests to the Aleph Prover API
Project-URL: Homepage, https://alephprover.logicalintelligence.com
Project-URL: Repository, https://github.com/logiq-ai/alephprover
Author: Logical Intelligence
License-Expression: MIT
License-File: LICENSE
Keywords: formal-verification,lean,lean4,proof-assistant,theorem-proving
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering :: Mathematics
Requires-Python: >=3.10
Requires-Dist: click>=8.0
Requires-Dist: httpx>=0.27
Description-Content-Type: text/markdown

# Aleph Prover CLI

Prove Lean4 theorems with the [Aleph Prover](https://alephprover.logicalintelligence.com) API from your terminal or from [Claude Code](https://claude.ai/code).

## Install

```bash
# 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

```bash
# 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](https://claude.ai/code):

```bash
# 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](https://alephprover.logicalintelligence.com/account) |
| `PROVER_API_URL` | No | `https://alephprover.logicalintelligence.com` | API base URL |

## Requirements

- Python >= 3.10
- [`uv`](https://docs.astral.sh/uv/) (for `uvx` usage) or `pip install alephprover`
- `git` (for applying patches)
- An Aleph Prover account with an API key
