Codex

ID codex · Company OpenAI

Use OpenAI’s Codex CLI as an automated theorem prover with Lean skills and MCP tooling. This prover uses the AgentProver with the CodexHarness.

Authentication

Codex is available on paid ChatGPT plans. Choose a plan and sign up if you don’t have an account. Install the Codex CLI and generate an ephemeral API token once on the host:

codex login

Check you are properly authenticated with:

open-atp auth-status codex

This writes credentials to ~/.codex/auth.json. By default the harness reads that file; pass it explicitly to override:

from pathlib import Path

from open_atp.harness import CodexHarness

CodexHarness(auth_file=Path("~/.codex/auth.json").expanduser())

The harness mounts the credential into the sandbox at run time so Codex can refresh its access token mid-session, billing against your ChatGPT subscription. See Tracking cost and usage for details.

Warning

Token expiration: The token in ~/.codex/auth.json expires roughly 10 days after it is minted, and it only renews when the Codex CLI runs on the host. A sandboxed run will fail if the token expires mid-run. Check the time remaining with open-atp auth-status, and run codex login on the host before a long benchmark.

Using the prover

Standard prover via Python API

The simplest way to run the prover is through standard_prover() which uses a standard configuration. 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("codex", 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 codex

Customizing the prover

To override knobs like model and effort, 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 CodexHarness
from open_atp.images import DEFAULT_IMAGE
from open_atp.provers import AgentProver

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=CodexHarness(effort="high"),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all CodexHarness configuration options.

Warning

Codex does not support all of the models available in the OpenAI API.

Harness details

By default, the Codex harness is equipped with:

  • Official Lean skills [8].

  • lean-lsp-mcp MCP server [2].

The agent prompt (below) is written into the working directory and read into $PROMPT. The Codex CLI is then invoked in non-interactive mode with $PROMPT as the input. See the script below for the full Codex CLI invocation.

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 the import oleans aren't
   materialized yet — run `lake env lean <file>` once to build them.
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 every file compiles
   cleanly. Do the final compile check per file with `lake env lean <file>`:
   exit code 0 and no output means it compiles. This is the exact command the
   grader uses, so it is the source of truth.

Tips:
- Use the lean-lsp tools (`mcp__lean-lsp__*`) as your primary feedback loop; they
  are far faster than compiling per change.
- Do NOT trust `lake build` as a compile check: the `.lean` files here are not
  lake library targets, so `lake build` reports `Build completed successfully
  (0 jobs)` without ever compiling them. Always confirm with
  `lake env lean <file>`, which compiles the file by path.
- 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."""
src/open_atp/harness/assets/scripts/codex_agent.sh
#!/usr/bin/env bash

# $PROMPT is exported by the AgentProver before this script runs (it reads
# agent_prompt.txt from the workdir). The backend has already cd'd into the
# workdir and symlinked .lake to the warm Mathlib cache.
#
# `codex exec` runs non-interactively; danger-full-access gives broad permissions
# (safe in the container). Codex doesn't auto-discover .mcp.json, so the lean-lsp
# MCP server is registered via -c overrides. The --json event stream goes to stdout.
#
# https://developers.openai.com/codex/cli/reference
# https://developers.openai.com/codex/config-advanced#one-off-overrides-from-the-cli

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"

Tracking cost and usage

The Codex CLI does not report per-run USD. Token totals from the turn.completed events are summed and the pricing table in COST_PER_MTOK is used to compute the cost in USD. This populates cost_usd in ProofResult. Usage within your plan’s quota is not billed. You can monitor plan consumption at Analytics.

Warning

Running a large number of proofs can quickly consume your plan’s 5 hour session quota.