DeepSeek

ID deepseek · Company DeepSeek

Use a DeepSeek model as an automated theorem prover. This prover runs on the OpenCode harness pinned to DeepSeek’s deepseek-v4-pro model. See OpenCode for harness details.

Authentication

DeepSeek bills against an API account. Sign up at the DeepSeek platform, fund it, and provide the key through the environment:

export DEEPSEEK_API_KEY=...

Check if the key is in your environment with:

open-atp auth-status deepseek

Alternatively, pass the key to the harness explicitly:

from open_atp.harness import OpenCodeHarness

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

Using the prover

Standard prover via Python API

The simplest way to run the prover is through standard_prover(), which pins the deepseek-v4-pro model on the OpenCode harness. Set DEEPSEEK_API_KEY in the host environment (or pass it to the harness explicitly). 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("deepseek", 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 deepseek

Customizing the prover

To override knobs like 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 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"))

Tracking cost and usage

Cost is captured from the OpenCode CLI’s per-call breakdown and summed into cost_usd on ProofResult (see Tracking cost and usage). You can also monitor DeepSeek consumption from the provider dashboard at DeepSeek Usage.