Running a Prover¶

An automated theorem prover takes a formal statement in Lean and attempts to fill all sorry uses. OpenATP supports multiple options for running a prover. In this guide, we begin by proving a trivial example theorem to test the compute backend and prover configuration. Next, we discuss all of the output generated by a prover run. Finally, we show how to run a prover programmatically with the Python API or from the command line.

Prerequisites¶

Docker installed and the open-atp:latest image built (see Running Locally with Docker).
A CLAUDE_CODE_OAUTH_TOKEN in your environment (see Claude Code authentication).

Note

This page uses DockerBackend for the compute backend and Claude Code for the prover in the example scripts. Alternatively, you can use the ModalBackend (Running Remotely with Modal) or another standard prover (Provers).

Testing compute and prover setup¶

OpenATP ships with small example theorems (see Examples) to make testing compute and prover setup easy. In the script below, we load the MUL_REORDER example task, configure the Claude Code prover, and then run the prover on the task.

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"))

assert result.success

Generating this proof may take 2-3 minutes on the first run. If the assert passes, you’ve successfully run your first automated theorem prover with OpenATP!

Inspecting a proof run¶

Proof result¶

The prove() method returns a ProofResult with many details about the prover run.

cost_usd and duration_s are useful for comparing different provers.
metadata contains prover-specific metadata.
verification contains the VerificationReport.

Here’s the output for the example above:

>>> result.cost_usd
0.617242
>>> result.duration_s
68.33680745901074
>>> result.metadata
{'harness': 'claude_code', 'model': 'claude-opus-4-8', 'effort': 'high',
 'input_tokens': 5701, 'output_tokens': 882, 'stop_reason': 'end_turn'}

Verification report¶

In addition to calling the prover to fill each sorry, prove() calls verify() to compile the resulting Lean proof and run deterministic checks. This generates the VerificationReport.

compiles indicates if the proof built successfully.
sorry_free indicates if all sorry uses were removed.
non_standard_axioms lists any axioms not in STANDARD_AXIOMS.
verified is true if all the above checks pass.

Here’s the output for the example above:

>>> result.verification.compiles
True
>>> result.verification.sorry_free
True
>>> result.verification.non_standard_axioms
()
>>> result.verification.verified
True

Prover output¶

In addition to returning a ProofResult, prove() writes output to output_dir. Here’s the complete output directory from the MUL_REORDER proof run example.

demo
├── logs
│   ├── result.json
│   └── stdout.txt
└── wd
    ├── .claude
    ├── .lake -> /workspace/.lake
    ├── .mcp.json
    ├── .plugins
    ├── agent_prompt.txt
    ├── agent.sh
    ├── lake-manifest.json
    ├── lakefile.toml
    ├── lean-toolchain
    └── MulReorder.lean

The logs subdirectory contains various logging files.

result.json — a JSON representation of ProofResult.
stdout.txt — logging from the prover (in the case of an AgentProver, this will be the JSONL output from the agent harness CLI).

The wd subdirectory is the agent’s working directory.

MulReorder.lean — the Lean file containing the theorem statement and proof
.claude, .plugins, .mcp.json — agent harness configurations
agent.sh — bash script used to call the agent harness
agent_prompt.txt — prompt supplied to the agent harness
lakefile.toml, lake-manifest.json, lean-toolchain — lake project files
.lake -> /workspace/.lake — forwards the Docker image’s cache into the working directory

Tip

The .lean files are the most relevant artifacts in the wd subdirectory. However, the working directory combined with the prover logs in stdout.txt can be a very valuable debugging resource.

Inspecting MulReorder.lean, we find the generated proof is a simple application of the ring tactic.

import Mathlib

/-! From *Mathematics in Lean*, C02 "Calculating": reorder a product of reals
using commutativity and associativity. -/

example (a b c : ℝ) : c * b * a = b * (a * c) := by
  ring

Run with Python API¶

The prove() method takes a ProofTask as input. Proof tasks can be constructed by individual .lean files or a full lake project.

Single files¶

When you only have individual .lean files, create_project() stages them into a pinned Mathlib skeleton to produce a complete LeanProject:

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.config import standard_prover
from open_atp.lean import ProofTask, create_project

project = create_project(["MyFile.lean"], dest="demo/project")
task = ProofTask(project=project)

prover = standard_prover("claude", backend=DockerBackend())
result = prover.prove(task, output_dir=Path("demo/run"))

The default skeleton used by create_project() uses v4.28.0 of the Lean toolchain and Mathlib. Use skeleton to supply a custom project skeleton.

Full lake projects¶

If you already have a full lake project, point LeanProject straight at the directory. By default, the prover fills sorry in every file that has one. Pass targets to ProofTask to focus on specific files (relative to the project root).

from pathlib import Path

from open_atp.backends.docker import DockerBackend
from open_atp.config import standard_prover
from open_atp.lean import LeanProject, ProofTask

project = LeanProject("path/to/lake/project")
task = ProofTask(project=project)

prover = standard_prover("claude", backend=DockerBackend())
result = prover.prove(task, output_dir=Path("demo/run"))

Warning

All ComputeBackends use the DEFAULT_IMAGE which pins v4.28.0 of the Lean toolchain and Mathlib. If your lake project uses different versions, prove() will raise a ToolchainMismatch or MathlibRevMismatch. Supply a custom Image to ComputeBackend via the image argument with lean_version and mathlib_rev matching your project. You also need to ensure the deployed Docker image has been built with the same versions.

Run with CLI¶

The open-atp prove command is a thin shell over the same API. Provide a path to the task, an output destination for the run, and a standard prover (see Provers). The task can be a single .lean file or a full lake project directory.

Run a single file:

$ open-atp prove Example.lean demo claude
╭────────────┬──────────────╮
│ status     │ ✓ verified   │
│ prover     │ agent        │
│ cost       │ $0.5123      │
│ time       │ 42s          │
│ output     │ demo         │
│ compiles   │ ✓            │
│ sorry-free │ ✓            │
│ axioms     │ ✓            │
╰────────────┴──────────────╯

Run a full lake project:

$ open-atp prove path/to/lake/project demo claude
╭────────────┬──────────────╮
│ status     │ ✓ verified   │
│ prover     │ agent        │
│ cost       │ $0.5123      │
│ time       │ 42s          │
│ output     │ demo         │
│ compiles   │ ✓            │
│ sorry-free │ ✓            │
│ axioms     │ ✓            │
╰────────────┴──────────────╯

See CLI Reference for the full reference.