open-atp 0.2.0

OpenATP is an open-source Python package providing a common interface for Automated Theorem Proving (ATP). OpenATP focuses on recent agentic ATP methods that prove formal statements in Lean. Each method runs in an isolated sandbox, either locally with Docker or remotely with Modal. OpenATP also provides benchmarking utilities to run methods on common datasets.

Installation

pip install open-atp

OpenATP runs each prover (e.g., Claude Code, Codex, OpenCode) in a Docker container. The image must be built before running any prover:

open-atp build-docker-image

Each prover has its own authentication requirements. See each prover page for its authentication instructions.

Quickstart

Complete the sorrys in a lake project (or a .lean file) from the CLI:

open-atp prove path/to/project runs/example claude

Or programmatically, here on a simple example theorem:

from open_atp import standard_prover
from open_atp.backends import DockerBackend
from open_atp.examples import EXAMPLE, example_task

prover = standard_prover("claude", backend=DockerBackend())
task = example_task(EXAMPLE.MUL_REORDER)

result = prover.prove(task, output_dir="runs/example")

Available provers

The ID is the standard prover name used by standard_prover, the CLI prove command's prover argument, and the benchmark command's -p/--provers option. Also see Provers.

Download common datasets

OpenATP provides utilities to download common proof-synthesis benchmarks (see Downloading a dataset). The available datasets are listed in the DATASET enum.

Citing

If you use OpenATP in your work, please cite it:

@software{openatp,
  title = {OpenATP: Open Automated Theorem Proving},
  author = {Henry Robbins},
  year = {2026},
  publisher = {GitHub},
  url = {https://github.com/henryrobbins/open-atp}
}

OpenATP includes provers with associated papers and bundles popular open-source tools for improving agentic theorem proving. Please see Citations for a comprehensive list of references.

Development

See AGENTS.md for development information.

License

MIT