`provers`¶

The concrete provers and the registry/factory over them. Each prover subclasses AutomatedProver and funnels its output through the shared Verifier. The agentic provers compose an agent harness (the agent concern) with a ComputeBackend (the compute concern).

Base¶

The base prover abstraction. An AutomatedProver is a candidate generator; the base class owns the shared lifecycle (the public prove: generate, then verify in the sandbox) so subclasses only implement _generate.

class open_atp.provers.base.AutomatedProver(*, backend: ComputeBackend, timeout_s: int = 1800)[source]¶

Generate candidate proofs, then verify them in a shared sandbox.

The sandbox image (its tag plus the Lean toolchain + Mathlib pins the shared verifier checks every project against) comes from backend – a prover inherits whatever image its backend runs.

Parameters:

backendComputeBackend: The one backend for this prover. Agentic provers reuse it (via a live session) for generation, then verify in that hot sandbox; Aristotle uses it only for the final check.
timeout_sint, default 1800: Wall-clock budget for the generation run, in seconds.

property max_duration_s: int¶

Maximum wall-clock duration of a healthy prove() run, in seconds.

The total wall-clock time is the sum of: - the proof generation budget - post-generation verification - and the backend’s overhead

abstractmethod auth_status() → AuthStatus[source]¶

Report the status of the credential required by this prover.

Returns:

AuthStatus: Where the credential lives, whether it is there, and when it expires.

prove(task: ProofTask, output_dir: Path | str) → ProofResult[source]¶

Full lifecycle: reject-on-mismatch, generate, verify, write the result.

The credential is checked up front: an expired one raises, and one with less than EXPIRY_WARNING left is logged as a warning – a run outlives that window – but does not stop the run.

Parameters:

taskProofTask: The unit of work: the lake project to complete, the optional targets to focus on, and any user_prompt guidance.
output_dirpathlib.Path or str: Caller-chosen output directory, populated as output_dir/{wd,logs}/: wd is the completed lake project (the proof output) and logs is the run record (the agent stdout.txt/stderr.txt, result.json, and any harness-specific rich logs).

Returns:

ProofResult: The outcome of the run, pointing at the populated wd and logs_dir.

Raises:

ToolchainMismatch: If the project’s toolchain differs from the backend image’s. Checked up front, before any run starts – so this raises rather than returning an empty result.
MathlibRevMismatch: If the project records a Mathlib revision that differs from the backend image’s. Checked up front, before any run starts.
MissingCredentials: If a credential the run needs is absent or already expired, or if the agent’s provider rejected the one it was given. Either way no proof was attempted, so this raises rather than returning an empty result.
ProvisionError: If the compute sandbox fails to come up (daemon down, image missing, capacity). Raised before generation, so the run never started.

class open_atp.provers.base.ProofResult(prover: str, verification: ~open_atp.verify.VerificationReport | None, output_dir: ~pathlib.Path, completed_files: dict[str, str] = <factory>, cost_usd: float | None = None, duration_s: float | None = None, metadata: dict[str, object] = <factory>, error: str | None = None, error_msg: str | None = None, status: ~open_atp.provers.base.ProofStatus = ProofStatus.ERROR)[source]¶

What a prover returns from AutomatedProver.prove().

The prover writes its artifacts into the caller-chosen output_dir, laid out as output_dir/{wd,logs}/: wd is the completed lake project (the proof output) and logs is the run record (the streamed agent stdout.txt, stderr.txt, result.json, and any harness-specific rich logs). This object just records where those live, plus the verification verdict and run metadata.

Parameters:

proverstr: Name of the prover that produced this result.
verificationVerificationReport or None: The shared verification of the completed project, or None when the run failed before a candidate could be verified (see error).
output_dirpathlib.Path: The run’s output directory. Holds the wd (proof project) and logs_dir (run record) subdirectories the prover populated.
completed_filesdict[str, str], optional: The completed .lean sources, keyed by file path relative to the project root. Defaults to an empty mapping.
cost_usdfloat, optional: Estimated USD cost of the run. None when the prover does not report cost.
duration_sfloat, optional: Wall-clock duration of the run, in seconds.
metadatadict[str, object], optional: Harness-specific run metadata (token counts, run summaries, …). Defaults to an empty mapping.
errorstr, optional: The failing exception’s class name; set when status is ERROR or TIMEOUT.
error_msgstr, optional: The failing exception’s message; set when status is ERROR or TIMEOUT.
statusProofStatus, default ProofStatus.ERROR: Status of the proof generation run.

property wd: Path¶

The completed working directory, output_dir/wd.

A complete lake project holding the completed .lean files – the proof output.

property logs_dir: Path¶

The run’s logs directory, output_dir/logs.

Holds the captured agent stream (stdout.txt), stderr.txt, result.json, and any harness-specific rich record (Vibe’s session log, ax-prover’s per-target logs, Aristotle’s events).

property success: bool¶

Whether the run produced a verified proof.

True iff verification exists and is verified.

to_dict() → dict[str, object][source]¶: JSON-ready view: inline files, verification, cost, and artifact paths.

class open_atp.provers.base.ProofStatus(*values)[source]¶: Coarse status for a ProofResult.

exception open_atp.provers.base.ProverError[source]¶: Parent Exception class for prover-side failure the run anticipates.

exception open_atp.provers.base.GenerationTimeout[source]¶

Bases: ProverError

The proof generation consumed its wall-clock budget before finishing.

Provers¶

The concrete candidate generators.

class open_atp.provers.agent_prover.AgentProver(*, backend: ComputeBackend, name: str | None = None, harness: Harness | None = None, skills: list[str] | None = None, timeout_s: int = 1800)[source]¶

Bases: AutomatedProver

Generate proofs by driving an agent CLI harness in a compute backend.

Composes an agent harness (the agent concern) with a ComputeBackend (the compute concern): the harness edits the staged .lean files in place, then the shared Verifier does the final compile/sorry/axiom check. Most entries in STANDARD_PROVERS are this prover on a different harness.

Parameters:

backendComputeBackend: The sandbox the agent runs in. Generation reuses it via a live session and verification runs in that same hot sandbox.
namestr, optional: The prover’s reported name (in log events and ProofResult.prover). Defaults to the harness’s name; the standard catalog passes the registry key so claude/leanstral report their user-facing name rather than the harness name (claude_code/vibe).
harnessHarness, optional: The harness to drive, carrying model/effort plus any harness-specific knobs. Defaults to ClaudeCodeHarness.
skillslist[str], default [“lean-proof”]: Skills to mount into the agent workdir, each a name (resolved from the vendored leanprover/skills catalog) or a full path to a SKILL.md tree. An empty list mounts none. Staged into every skill-supporting harness’s location; ignored by ax-prover.
timeout_sint, default 1800: Wall-clock budget for the generation run, in seconds.

Examples

Construct the prover directly, wiring up a harness and a backend:

>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.harness import CodexHarness
>>> from open_atp.provers.agent_prover import AgentProver
>>> backend = DockerBackend()
>>> prover = AgentProver(harness=CodexHarness(effort="high"), backend=backend)
>>> prover.harness.model
'gpt-5.5'

Or build the same prover from the standard catalog by name, taking its baked-in defaults (see standard_prover()):

>>> from open_atp import standard_prover
>>> prover = standard_prover("codex", backend=DockerBackend())
>>> prover.name, prover.harness.name
('codex', 'codex')

Complete a task’s sorrys with prove(), here on a bundled example (this runs the agent in Docker and bills it):

>>> import tempfile
>>> from open_atp.examples import EXAMPLE, example_task
>>> task = example_task(EXAMPLE.MUL_REORDER)
>>> result = prover.prove(task, tempfile.mkdtemp())
>>> result.success
True

property prover_prompt: str¶: The prover’s own prompt handed to the agent, before any user prompt.

auth_status() → AuthStatus[source]¶

Report the credential the agent CLI runs on.

Returns:

AuthStatus: The agent harness’s own credential status.

class open_atp.provers.numina.NuminaProver(*, backend: ComputeBackend, skills: list[str] | None = None, max_rounds: int = 20, max_consecutive_limits: int = 2, oauth_token: str | None = None, helper_env_keys: tuple[str, ...] = ('GEMINI_API_KEY', 'OPENAI_API_KEY', 'LEAN_LEANDEX_API_KEY', 'ANTHROPIC_API_KEY'), guard_statements: bool = True, on_statement_change: Literal['error', 'warn'] = 'error', timeout_s: int = 1800, env: dict[str, str] | None = None)[source]¶

Bases: AgentProver

Run the Numina coordinator/subagent scaffold as an AgentProver.

Numina’s vendored scaffold – coordinator prompt, skills, and subagent prompts – is staged into the sandbox’s .claude/ tree; generation and the shared Verifier work exactly as in the base agent prover.

The harness is not configurable: Numina is claude-CLI driven and ships its own scaffold in place of plugins.

Parameters:

backendComputeBackend: The sandbox the agent runs in. Generation reuses it via a live session and verification runs in that same hot sandbox.
skillslist[str], optional: Extra named/path skills to mount alongside Numina’s vendored scaffold. Defaults to none – Numina’s coordinator skill is staged from vendor/numina/skills, not this list.
max_roundsint, default 20: Maximum number of coordinator rounds before the run stops.
max_consecutive_limitsint, default 2: Reset (start a fresh session) after this many consecutive LIMIT rounds.
oauth_tokenstr, optional: The CLAUDE_CODE_OAUTH_TOKEN to forward into the sandbox; None (default) reads it from the host env var.
helper_env_keystuple[str, …], optional: Helper-skill credentials forwarded into the sandbox when present in the host env; skills degrade/skip when their key is absent. Defaults to the Leandex, Gemini, OpenAI, and Anthropic key names.
guard_statementsbool, default True: Whether to snapshot the target theorems and reject runs that weaken or delete them.
on_statement_change{“error”, “warn”}, default “error”: Behavior on a weakened/deleted target theorem: error stops the run and restores the originals; warn restores and continues. The default rejects, which is the safe choice.
timeout_sint, default 1800: Wall-clock budget for the generation run, in seconds.
envdict[str, str], optional: Extra literal environment variables forwarded into the agent sandbox (Numina pins its harness, so its env knobs live here). Defaults to no extra variables.

Examples

Construct the prover directly:

>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.provers.numina import NuminaProver
>>> backend = DockerBackend()
>>> prover = NuminaProver(backend=backend)
>>> prover.max_rounds
20

Or build the same prover from the standard catalog by name, taking its baked-in defaults (see standard_prover()):

>>> from open_atp import standard_prover
>>> prover = standard_prover("numina", backend=DockerBackend())
>>> prover.name
'numina'

Complete a task’s sorrys with prove(), here on a bundled example (this runs the Numina scaffold in Docker and bills it):

>>> import tempfile
>>> from open_atp.examples import EXAMPLE, example_task
>>> task = example_task(EXAMPLE.INTER_UNION_DISTRIB)
>>> result = prover.prove(task, tempfile.mkdtemp())
>>> result.success
True

property prover_prompt: str¶

The prover’s own prompt, handed to the agent before any user prompt.

Numina’s coordinator scaffold plus the round protocol.

class open_atp.provers.aristotle.AristotleProver(*, backend: ComputeBackend, api_key: str | None = None, allow_agent_questions: bool = False, max_connection_retries: int = 5, retry_backoff_seconds: float = 5.0, poll_interval_s: float = 15.0, timeout_s: int = 1800)[source]¶

Bases: AutomatedProver

Prove by handing the whole project to Harmonic’s hosted Aristotle agent.

Generation happens over the network (submit the lake project, wait, download the result archive, unpack it over the workdir); the shared Verifier then runs the same local compile/sorry/axiom check. Generation is network-only, so the backend is used solely for that final check – unlike the agentic provers, there is no live session to reuse.

Parameters:

backendComputeBackend: The sandbox used only for the final verify; Aristotle generates over the network, so there is no live session to reuse.
api_keystr, optional: The Harmonic API key. None (default) reads it from the host ARISTOTLE_API_KEY env var.
allow_agent_questionsbool, default False: Whether to let the hosted agent ask clarifying questions. This is a headless API path, so a prompt for stdin would hang the run.
max_connection_retriesint, default 5: Bounds retries of each API call when a connection drops. The hosted run lives server-side, so a dropped connection is recoverable: re-fetch rather than reporting the run failed.
retry_backoff_secondsfloat, default 5.0: Initial sleep between retries of a failed call, doubling (capped) between tries.
poll_interval_sfloat, default 15.0: Seconds between polls of the task’s status while waiting for generation.
timeout_sint, default 1800: Hard wall-clock cap on the generation wait, in seconds. When it elapses we stop waiting and verify whatever Aristotle has produced so far; if that does not verify the run’s status is TIMEOUT. The run keeps going and billing server-side regardless – this only bounds the client.

Examples

Construct the prover directly (network-only generation, so the backend is just the verify backend):

>>> from open_atp.backends.docker import DockerBackend
>>> from open_atp.provers.aristotle import AristotleProver
>>> backend = DockerBackend()
>>> prover = AristotleProver(backend=backend)
>>> prover.name
'aristotle'

Or build the same prover from the standard catalog by name, taking its baked-in defaults (see standard_prover()):

>>> from open_atp import standard_prover
>>> prover = standard_prover("aristotle", backend=DockerBackend())
>>> prover.name
'aristotle'

Complete a task’s sorrys with prove(), here on a bundled example (this hits the hosted Aristotle API, needing ARISTOTLE_API_KEY, and runs Docker for the verify):

>>> import tempfile
>>> from open_atp.examples import EXAMPLE, example_task
>>> task = example_task(EXAMPLE.ABS_MUL_LT)
>>> result = prover.prove(task, tempfile.mkdtemp())
>>> result.success
True

property prover_prompt: str¶: The prover’s own prompt handed to Aristotle, before any user prompt.

auth_status() → AuthStatus[source]¶

Report the ARISTOTLE_API_KEY the hosted API is called with.

Returns:

AuthStatus: The API key status, read from api_key constructor or host environment.

exception open_atp.provers.aristotle.ServiceError[source]¶: The hosted Aristotle service produced no candidate to verify.

Standard catalog¶

The standard catalog names each ready-to-run default prover and builds it against a compute backend. standard_prover() maps a catalog name to a constructed AutomatedProver, wiring in the shared image/toolchain from the backend; a caller then drives it directly via prove(), which returns a ProofResult with verification and cost. Agentic provers run generation in a live session over that backend and verify in the same hot sandbox. This is the top-level surface re-exported from open_atp itself.

standard_provers() lists the accepted names. Each builds its class’s baked-in defaults — to customize any knob, construct the prover class directly.

open_atp.config.standard_prover(name: str, *, backend: ComputeBackend) → AutomatedProver[source]¶

Construct a standard default prover name against backend.

name is a STANDARD_PROVERS key, as listed by standard_provers(). The prover is built with its class’s baked-in defaults; to customize any knob (model, effort, skills, …), construct the prover class directly instead.

The sandbox image (and the toolchain + Mathlib pins projects are checked against) comes from backend, not a parameter here.

Examples

>>> from open_atp.backends.docker import DockerBackend
>>> prover = standard_prover("claude", backend=DockerBackend())
>>> prover.harness.model
'claude-opus-4-8'

open_atp.config.standard_provers() → list[str][source]¶: The names standard_prover() accepts: the STANDARD_PROVERS keys.

open_atp.config.STANDARD_PROVERS: dict[str, dict[str, object]] = {'aristotle': {'type': 'aristotle'}, 'axproverbase': {'harness': {'type': 'axproverbase'}, 'type': 'agent'}, 'claude': {'harness': {'type': 'claude_code'}, 'type': 'agent'}, 'codex': {'harness': {'type': 'codex'}, 'type': 'agent'}, 'deepseek': {'harness': {'auth': 'api_key', 'model': 'deepseek-v4-pro', 'provider': 'deepseek', 'type': 'opencode'}, 'type': 'agent'}, 'grok': {'harness': {'auth': 'login', 'model': 'grok-4.5', 'provider': 'xai', 'type': 'opencode'}, 'type': 'agent'}, 'kimi': {'harness': {'type': 'kimi'}, 'type': 'agent'}, 'leanstral': {'harness': {'type': 'vibe'}, 'type': 'agent'}, 'numina': {'type': 'numina'}, 'spark': {'harness': {'auth': 'api_key', 'model': 'muse-spark-1.1', 'provider': 'meta', 'type': 'opencode'}, 'type': 'agent'}}¶: The standard catalog: a friendly name -> the canonical prover spec for that ready-to-run default, and the source of truth for which names the CLI accepts. Most entries are the shared AgentProver on a different harness – several share the opencode harness, differing only in provider and auth strategy – and the rest are standalone provers. Build one with standard_prover().

provers¶

Base¶

Provers¶

Standard catalog¶

`provers`¶