aristotlelib 2.0.0

Aristotle SDK - Python library for automated theorem proving with Lean

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

Quick Start

# 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 for fast, reliable Python package management.

Run Aristotle directly without a separate install step:

uvx --from aristotlelib@latest aristotle --version

Or install it into your environment:

uv pip install aristotlelib

Using pip

pip install aristotlelib

To upgrade:

pip install --upgrade aristotlelib

Authentication

To use Aristotle, you need an API key.

1. Sign up or log in at aristotle.harmonic.fun.
2. Go to Dashboard → API 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:

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:

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:

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

CLI Quick Reference

Fill sorries in a Lean project:

aristotle submit "Fill in all sorries in this project" --project-dir ./my-lean-project --wait

Formalize a document:

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

List your recent projects:

aristotle list --limit 10

Download a project's files:

aristotle download <project-id> --destination result.tar.gz