Metadata-Version: 2.4
Name: aristotlelib
Version: 1.0.0
Summary: Aristotle SDK - Python library for automated theorem proving with Lean
Author: Harmonic
Maintainer: Harmonic
Project-URL: Homepage, https://aristotle.harmonic.fun
Requires-Python: >=3.10
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: pydantic>=2.0.0
Requires-Dist: httpx>=0.24.0
Requires-Dist: pathspec>=0.11.0
Provides-Extra: dev
Requires-Dist: pytest>=8.4.0; extra == "dev"
Requires-Dist: pytest-asyncio>=1.0.0; extra == "dev"
Dynamic: license-file

# Aristotle - The Era of Vibe Proving is Here

The Aristotle SDK is a Python library and command-line tool for interacting with the Aristotle API. Aristotle is capable of proving and formally verifying graduate and research level problems in math, software, and more.

[Sign up for access and view the complete documentation at aristotle.harmonic.fun](https://aristotle.harmonic.fun)

## Quick Start

```bash
# Install
uv pip install aristotlelib

# Authenticate
export ARISTOTLE_API_KEY="your-api-key-here"

# Submit a Lean project for sorry filling
aristotle submit "Fill in all sorries" --project-dir ./my-lean-project --wait

# Formalize a math paper into Lean
aristotle formalize paper.tex --wait --destination output.tar.gz
```

## Installation

**Requires Python 3.10 or later.** Pick one of the following methods.

### Using `uv` (recommended)

We recommend [`uv`](https://docs.astral.sh/uv/) for fast, reliable Python package management.

Run Aristotle directly without a separate install step:

```bash
uvx --from aristotlelib@latest aristotle --version
```

Or install it into your environment:

```bash
uv pip install aristotlelib
```

### Using `pip`

```bash
pip install aristotlelib
```

To upgrade:

```bash
pip install --upgrade aristotlelib
```

## Authentication

To use Aristotle, you need an API key.

1. Sign up or log in at [aristotle.harmonic.fun](https://aristotle.harmonic.fun).
2. Go to [Dashboard → API Keys](https://aristotle.harmonic.fun/dashboard/keys) and create a new key.

### Save it as an environment variable (recommended)

Set your key once so it's available automatically in every terminal session.

#### macOS / Linux

Open your terminal and run these two commands, replacing `your-api-key-here` with your actual key:

```bash
echo 'export ARISTOTLE_API_KEY="your-api-key-here"' >> ~/.zshrc
source ~/.zshrc
```

The first command saves the key to your shell startup file (`~/.zshrc`) so every new terminal session will have it. The second command loads it into your current session right away.

> If you use **bash** instead of zsh, replace `~/.zshrc` with `~/.bashrc` in both commands.

#### Windows

Open **PowerShell** and run:

```powershell
setx ARISTOTLE_API_KEY "your-api-key-here"
```

Then **close and reopen** PowerShell for the change to take effect.

### Pass it directly to a command

Alternatively, you can add `--api-key` to any command without saving it:

```bash
aristotle submit "My prompt" --api-key your-api-key-here
```


## CLI Quick Refernece

Fill sorries in a Lean project:
```bash
aristotle submit "Fill in all sorries in this project" --project-dir ./my-lean-project --wait
```

Formalize a document:

```bash
aristotle formalize paper.tex --wait --destination output.tar.gz
```

List your recent projects:

```bash
aristotle list --limit 10
```

Get a project's result:

```bash
aristotle result <project-id> --destination result.tar.gz
```
