OpenCode

Use OpenCode as an automated theorem prover with common skills and MCP tooling for working with Lean. OpenCode is an open-source coding-agent harness with many supported model providers. OpenATP supports OpenCode through the AgentProver and the OpenCodeHarness.

Tip

We recommend Claude Code and Codex prover over using OpenCode with the anthropic or openai providers. These provers use their native agent harness and are billed against subscription plans.

Authentication

Each OpenCode provider requires authentication. OpenATP supports two authentication strategies: API key and login. The harness’s auth argument selects the strategy.

If your provider supports authentication via OAuth with billing against a subscription plan, use the OpenCode login strategy to avoid paying for API usage. Otherwise, use the API key strategy.

API key

By default, the harness will look for the provider’s canonical API key in the host environment. E.g., the deepseek provider uses DEEPSEEK_API_KEY. You can also set the key explicitly using the api_key argument.

from open_atp.harness import OpenCodeHarness

OpenCodeHarness(provider="deepseek", model="deepseek-v4-pro", api_key="sk-...")

OpenCode Login

Alternatively, you can authenticate with OpenCode login. Run the following command command and select your provider from the dropdown.

opencode auth login

This generates the necessary authentication credentials on your machine. You can then use the harness with the auth="login" argument to forward the credentials into the agent sandbox.

from open_atp.harness import OpenCodeHarness

OpenCodeHarness(provider="deepseek", model="deepseek-v4-pro", auth="login")

Using the harness

The OpenCode harness can be used directly with AgentProver for automated theorem proving. Once you’ve selected a provider and an authentication strategy, just select a model and effort level. Note the model must be supported on the chosen provider. Here, we prove the MUL_REORDER example theorem:

from pathlib import Path

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

task = example_task(EXAMPLE.MUL_REORDER)
prover = AgentProver(
    harness=OpenCodeHarness(provider="deepseek", model="deepseek-v4-pro", effort="medium"),
    backend=DockerBackend(image=DEFAULT_IMAGE),
)
result = prover.prove(task, output_dir=Path("demo"))

Harness details

By default, the OpenCode 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 OpenCode CLI is then invoked in non-interactive mode with $PROMPT as the input. See the script below for the full OpenCode 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/opencode_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.
#
# `opencode run` runs non-interactively; opencode.json (written by the harness)
# configures the model provider and the lean-lsp MCP server. The JSON event
# stream goes to stdout.
#
# --auto auto-approves every permission (safe in the container). Without it a
# prompt is auto-*rejected* and opencode tears the session down mid-turn.
#
# https://opencode.ai/docs/cli/#run-1
#
# With auth='login' the harness mounts a minimal opencode data dir at
# $HOME/.opencode-data, so opencode reads the credential from there instead
# of an API-key env var.
[ -d "$HOME/.opencode-data" ] && export XDG_DATA_HOME="$HOME/.opencode-data"

opencode run --dir /workspace/wd --format json --auto \
    --model '<<PROVIDER>>/<<MODEL>>' \
    "$PROMPT"

See the API Reference for all OpenCodeHarness configuration options.

Tracking cost and usage

The OpenCode CLI reports a per-step cost and token breakdown for each provider call. The cost is summed to populate cost_usd in ProofResult. You can also monitor consumption from your provider’s usage dashboard — each model page links its own.