Claude Code

ID claude · Company Anthropic

Use Claude Code as an automated theorem prover with common skills and MCP tooling for working with Lean. This prover uses the AgentProver with the ClaudeCodeHarness.

Authentication

Claude Code is included with every paid Claude plan. Choose a Claude plan and sign up if you don’t have an account. Install the Claude Code CLI and generate a long-lived OAuth token once on the host:

claude setup-token

Check you are properly authenticated with:

open-atp auth-status claude

By default, the harness will read CLAUDE_CODE_OAUTH_TOKEN from the host environment. It is recommended to define this in a .env file in your project root.

CLAUDE_CODE_OAUTH_TOKEN=sk-ant-oat01-...

Alternatively, pass the token to the harness explicitly:

from open_atp.harness import ClaudeCodeHarness

ClaudeCodeHarness(oauth_token="sk-ant-oat01-...")

The harness forwards CLAUDE_CODE_OAUTH_TOKEN into the sandbox at run time, billing against your Claude plan (not the API). See Tracking cost and usage.

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("claude", 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 claude

Customizing the prover

To override knobs like model and effort, construct the class directly. In this example, we use the claude-opus-4-8 model with high effort:

from pathlib import Path

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

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=ClaudeCodeHarness(model="claude-opus-4-8", effort="high"),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

See the API Reference for all ClaudeCodeHarness configuration options.

Warning

Claude Code does not support all of the models available in the Claude API.

Harness details

By default, the Claude Code harness is equipped with:

  • Official Lean skills [8].

  • Lean4 Claude Code plugin [3].

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

The agent prompt (below) is written into the working directory and read into $PROMPT. The Claude Code CLI is then invoked in non-interactive mode with $PROMPT as the input. See the script below for the full Claude Code 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/claude_code_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.
#
# bypassPermissions skips all permission prompts (safe in the container);
# IS_SANDBOX=1 (set by the prover) lets that mode run non-interactively.
# .mcp.json registers the lean-lsp MCP server; --strict-mcp-config restricts
# the agent to exactly those servers. The stream-json event stream goes to stdout.
#
# The harness appends zero or more `--plugin-dir .plugins/<name>` flags below (one
# per mounted plugin, staged under .plugins/<name>); --plugin-dir is the only way
# to load a local plugin in a headless `-p` run, and its SessionStart hooks +
# subagents fire there. None are appended when the bundle mounts no plugins.
#
# https://code.claude.com/docs/en/cli-reference
# https://code.claude.com/docs/en/mcp#project-scope

claude -p "$PROMPT" \
    --output-format stream-json --verbose \
    --permission-mode bypassPermissions \
    --mcp-config .mcp.json --strict-mcp-config \
    --model '<<MODEL>>' --effort '<<EFFORT>>'<<PLUGIN_FLAGS>>

Tracking cost and usage

The Claude Code CLI’s JSON event stream reports per-run USD directly (total_cost_usd in the final result object). This populates cost_usd in ProofResult. Note that this cost is based on API rates. Usage within your plan’s quota is not billed. You can monitor plan consumption at Usage.

Warning

There are plans to migrate the Claude Agent SDK and claude -p non-interactive usage to no longer count towards Claude plan usage limits. This was originally planned for June 15, 2026. It has been delayed to a later date. See this article.

Warning

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