AristotleProver

The AristotleProver wraps Harmonic’s hosted Aristotle API. No agentic sandbox is needed for generation — the lake project is handed to the hosted agent via aristotlelib (submit → wait → download), the returned archive is unpacked over the workdir, and the shared Verifier does the final check in a local Docker sandbox. This is the platform’s simplest end-to-end slice.

Authentication

The prover reads the Harmonic API key from the ARISTOTLE_API_KEY environment variable (or pass it explicitly as AristotleProver api_key). Set it on the host:

export ARISTOTLE_API_KEY=...

or add it to a .env file in your project.

Usage

from open_atp.backends.docker import DockerBackend
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers.aristotle import AristotleProver

backend = DockerBackend(image=DEFAULT_IMAGE)
prover = AristotleProver(backend=backend)

The remote interaction is isolated in AristotleProver._submit_and_download, so tests can stand in a fake result without touching the network or an API key. See Running a prover for an end-to-end run and AristotleProver in the provers reference for configuration.

The prompt submitted to the hosted agent is Aristotle’s own prover prompt, with the task’s optional user_prompt appended under an Additional instructions heading when set (the agent CLI harnesses share a longer, tool-specific prover prompt instead):

Aristotle prover prompt

    "Complete every `sorry` in this Lean project. Make the project compile and be "
    "sorry-free without introducing new axioms; do not weaken or delete the stated "
    "theorems."
)

Note

Aristotle runs are billed by Harmonic against your ARISTOTLE_API_KEY. Verification still happens locally in your own Docker sandbox.