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 an API key from the environment variable named by api_key_env (default ARISTOTLE_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, DockerConfig
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers.aristotle import AristotleProver, AristotleProverConfig

backend = DockerBackend(DockerConfig(image=DEFAULT_IMAGE))
config = AristotleProverConfig()
prover = AristotleProver(config, verification_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 AristotleProverConfig in the provers reference for configuration.

The prompt submitted to the hosted agent is the task’s instructions when set, otherwise Aristotle’s own default prompt (the agent CLI harnesses share a longer, tool-specific prompt instead):

Default Aristotle 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.