Codex¶

The Codex prover is the AgentProver on the CodexHarness — OpenAI’s Codex CLI driving the sorrys in a sandbox with the lean-lsp-mcp server. The shared Verifier does the final compile / sorry / axiom check. See Provers for the staging/diff lifecycle every agent harness shares.

Usage¶

from open_atp.backends.docker import DockerBackend, DockerConfig
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers import AgentProver, AgentProverConfig

backend = DockerBackend(DockerConfig(image=DEFAULT_IMAGE))
config = AgentProverConfig(
    harness="codex",
    model="gpt-5.5",
    effort="high",
)
prover = AgentProver(config, verification_backend=backend)

Or by registry spec through get_prover() / the CLI: agent:codex. Because Codex authenticates through ChatGPT/OpenAI it must run an OpenAI model, so the agent:codex spec defaults model to gpt-5.5 rather than the AgentProverConfig Anthropic default.

Harness details¶

Codex does not auto-discover .mcp.json, so configure_wd mounts the bundle’s skills — the host-agnostic leanprover/skills — under .agents/skills/ and the lean-lsp MCP server is wired through -c overrides on the command line instead of a config file. The launch script (assets/scripts/codex_agent.sh) runs:

codex exec --json --skip-git-repo-check \
    --sandbox danger-full-access \
    --model '<MODEL>' \
    -c 'mcp_servers.lean-lsp.command="lean-lsp-mcp"' \
    -c 'mcp_servers.lean-lsp.args=[]' \
    -c 'model_reasoning_effort="<EFFORT>"' \
    "$PROMPT"

codex exec runs non-interactively; danger-full-access grants the broad permissions the in-place edits need (safe in the container). Note effort is passed via the model_reasoning_effort override, not a --effort flag. The --json event stream goes to stdout.

$PROMPT is the task’s instructions when set, otherwise the shared default agent prompt baked into the AgentProver:

Default agent prompt

The working directory is a complete Lean 4 lake project. One or more `.lean`
files contain `sorry` (or `admit`) placeholders standing in for proofs that have
not been written yet. Replace every such placeholder with a real proof so the
project compiles cleanly and depends on no axioms beyond Lean's standard set.

Hard rules:
- Do not weaken, rename, restate, or delete any theorem, lemma, `def`,
  `structure`, or signature. Only fill in proof bodies (the part after `:=` /
  `by` that is currently `sorry`). Changing a statement to make it easier to
  prove is failure, not success.
- No new axioms and no `sorry`/`admit`/`native_decide`-on-false escapes. The
  finished proof must type-check honestly. The only acceptable axioms are Lean's
  standard `propext`, `Classical.choice`, and `Quot.sound`.
- Stay inside this working directory; do not read or write files outside it.
- Do not edit `lakefile.toml`/`lakefile.lean`, `lean-toolchain`, or
  `lake-manifest.json` — they pin the toolchain and dependencies and must match
  the verification environment.

Workflow:
1. Find the work: search for `sorry` across the `.lean` source files (e.g.
   `rg -n '\\bsorry\\b'`). Read each file containing one to understand the
   statement, the hypotheses, and the relevant imports.
2. Confirm the lean-lsp MCP server is live before relying on it: call
   `mcp__lean-lsp__lean_diagnostic_messages` on a file you have not yet edited.
   `success:true, items:[]` means it compiles cleanly; real errors come back as
   `items`. `success:false, items:[]` usually means imports aren't built yet —
   run `lake build` for the relevant modules first.
3. Write a proof for one `sorry` at a time. Mathlib is available; prefer library
   lemmas, `simp`, `omega`, `linarith`, `exact?`/`apply?` suggestions, and
   `aesop` over long bespoke arguments.
4. After each edit, re-check that file with
   `mcp__lean-lsp__lean_diagnostic_messages` and iterate until it is clean.
5. When a file looks done, verify it has no stubbed proofs with
   `mcp__lean-lsp__lean_verify` — the reported axioms must NOT contain `sorryAx`.
6. Repeat until no `.lean` file contains a `sorry` and the whole project builds
   (`lake build`).

Tips:
- Use the lean-lsp tools (`mcp__lean-lsp__*`) as your primary feedback loop; they
  are far faster than a full `lake build` per change. Use `lake build` to
  materialize oleans for imports and as the final whole-project check.
- If a goal looks false or unprovable from the given hypotheses, re-read the
  statement: you likely misread a binder or a coercion. Do not "fix" it by
  changing the statement — finish the proof as stated.
- Non-trivial proofs routinely take many rounds of compile-error fixing. Keep
  iterating against the diagnostics rather than guessing."""

Authentication¶

Codex is available on paid ChatGPT plans — compare plans at ChatGPT pricing and monitor consumption at Analytics. Authenticate the Codex CLI once on the host:

codex login

This writes credentials to ~/.codex. The harness exposes that directory inside the sandbox at run time so Codex can refresh its access token mid-session, billing against your ChatGPT subscription.

Cost tracking¶

The Codex CLI does not report per-run USD. parse sums token totals from the turn.completed events (tolerating the input_tokens / inputTokens / prompt_tokens field-name variants) and leaves cost_usd None, so the prover estimates USD from the pricing table in COST_PER_MTOK. Keep that table aligned with current OpenAI API prices.