AxProverBase

ID axproverbase · Company Axiomatic AI

AxProverBase [6] is a self-contained LangGraph Lean agent with its own proposer → builder → reviewer → memory loop. This prover uses the AgentProver with the AxProverBaseHarness.

Authentication

Billing is directly against an API provider. By default the harness reads the provider’s key from the host environment:

export ANTHROPIC_API_KEY=...

Check if the key is in your environment with:

open-atp auth-status axproverbase

Alternatively, pass the key to the harness explicitly:

from open_atp.harness import AxProverBaseHarness

AxProverBaseHarness(provider_api_key="sk-...")

The provider is inferred from the model prefix, and the harness forwards the key into the sandbox under its canonical env var (ANTHROPIC_API_KEY, OPENAI_API_KEY, or GOOGLE_API_KEY). See Tracking cost and usage for details.

Using the prover

Standard prover via Python API

The simplest way to run the prover is through standard_prover() which uses a standard configuration pointing at the claude-opus-4-8 model. Either set ANTHROPIC_API_KEY in the host environment or pass it explicitly to the harness. Here, we prove the MUL_REORDER example theorem:

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.config import standard_prover
from open_atp.examples import EXAMPLE, example_task

task = example_task(EXAMPLE.MUL_REORDER)
prover = standard_prover("axproverbase", backend=DockerBackend())
result = prover.prove(task, output_dir=Path("demo"))

Standard prover via CLI

The standard prover can also be run from the CLI:

open-atp prove path/to/task.lean output_dir axproverbase

Customizing the prover

To override knobs like model, effort, and max_iterations, construct the class directly.

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.examples import EXAMPLE, example_task
from open_atp.harness import AxProverBaseHarness
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers import AgentProver

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=AxProverBaseHarness(
        model="claude-opus-4-8",
        effort="high",
        max_iterations=None,  # None keeps ax-prover's own default of 50; set an int to cap
    ),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all AxProverBaseHarness configuration options.

Harness details

AxProverBase has its own Lean tooling. It doesn’t use any of the skills or the Lean LSP MCP server [8] used by the other agent harnesses. See the script below for the full ax-prover CLI invocation.

src/open_atp/harness/assets/scripts/axprover_agent.sh

#!/usr/bin/env bash
set -euo pipefail

# $PROMPT is exported by the AgentProver before this script runs but is unused:
# ax-prover ships its own prompts. The backend has already cd'd into the workdir
# and symlinked .lake to the warm Mathlib cache.
#
# The Harness contract is project-wide, while ax-prover needs a target, so we
# self-discover every .lean carrying a `sorry` (skipping the warm .lake cache)
# and prove each in turn.
#
# Notes:
#   * --config is a TOP-LEVEL flag and MUST precede the `prove` subcommand. The
#     CLI's --config is argparse action="append" with default ["default.yaml"], so
#     passing axprover.yaml *appends* to (does not replace) the bundled default.yaml:
#     the effective merge is [default.yaml, axprover.yaml]. AxProverBaseHarness relies on
#     this (it overrides only deltas) and works around the deep-merge it implies --
#     see AxProverBaseHarness._render_config.
#   * --skip-build reuses the warm Mathlib .lake instead of re-running lake build
#     (the same assumption the other harnesses make).
#   * --overwrite re-proves even files ax-prover thinks are already done.
#   * `|| true` keeps one unprovable file from aborting the rest; the final
#     Verifier pass is the source of truth either way.
#   * -o writes ax_output.<target>.json: per-target {success, error, summary,
#     input_tokens, output_tokens, ...}. AxProverBaseHarness.parse_result sums the token fields
#     across these files for cost (the pinned fork commit adds the usage fields).
#   * ax-prover logs are human-readable (not the JSONL the parsers consume), so we
#     tee each run's stdout+stderr to ax_prover.<target>.log. The file lands in the
#     workdir and is pulled back with it (Modal) / lives on the bind mount (Docker),
#     so the logs survive even when the harness discards the stream. PYTHONUNBUFFERED
#     defeats CPython's block-buffering of a piped stdout so the tee is line-fresh.
#
# https://github.com/henryrobbins/ax-prover-base

export PYTHONUNBUFFERED=1

while IFS= read -r f; do
  [ -z "$f" ] && continue
  # Strip the leading ./ that `grep -rl . ` prepends: ax-prover derives a module
  # path via file_path.replace("/", ".") and a leading ./ corrupts it (-> ..Module),
  # which then resolves to a bogus file and hides every sorry ("No unproven found").
  f="${f#./}"
  safe=$(printf '%s' "$f" | tr '/.' '__')
  # `|| true` is on the pipeline: with `set -o pipefail` a failing ax-prover still
  # lets the loop continue, and tee captures the full log either way.
  ax-prover --config axprover.yaml prove "$f" \
    --folder . \
    --skip-build \
    --overwrite \
    -o "ax_output.${safe}.json" 2>&1 | tee "ax_prover.${safe}.log" || true
done < <(grep -rl --include='*.lean' '\bsorry\b' . | grep -v '/\.lake/' || true)

Tracking cost and usage

The ax-prover CLI does not report cost by default. We manually log input / output tokens to ax_output.<target>.json files, which are summed and combined with pricing estimates in COST_PER_MTOK to populate cost_usd in ProofResult. Those files carry no cache breakdown, so the whole input is priced at the uncached rate and cost_usd is an upper bound. You can also monitor consumption from your provider’s usage dashboard. For example, Anthropic’s dashboard is at Anthropic Usage.