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.
- Sign up or log in at aristotle.harmonic.fun.
- 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
~/.zshrcwith~/.bashrcin 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
2 maintainers
Metadata
2 maintainers
Release files for aristotlelib 2.1.0
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| aristotlelib-2.1.0-py3-none-any.whl | Python 3 | none | any | Details |
Release files / aristotlelib-2.1.0-py3-none-any.whl
| Download URL | aristotlelib-2.1.0-py3-none-any.whl |
|---|---|
| Size | 30.9 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
f290c8e0b74b15b5b5b432db6dd7915adc8f49fe83efef0fd2f2ea53b5c33555
|
|
BLAKE2b-256 checksum How to use checksums |
c5631d25b34c331deee0e667881f81b5760d4d9c10f4f787cb8c6e0992ed5c16
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
Yes |
| Uploaded via |
twine/6.1.0 CPython/3.13.7
|
Provenance
Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.
PyPI Publish Attestation
PyPI verified that this artifact, at this checksum, originated from the publisher listed below.
Signed by GitHub Actions, verified by PyPI on Jun 18, 2026.
Transparency log
