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.

Prover	ID	Skills	MCP	Paper	Source
Claude Code	claude	leanprover, lean4	✓	—	—
Codex	codex	leanprover	✓	—	GitHub
OpenCode	opencode	leanprover	✓	—	GitHub
AxProverBase	axproverbase	—	✗	Requena et al. 2026	GitHub
Leanstral	leanstral	leanprover	✓	Leanstral (blog)	HuggingFace
Numina	numina	—	✓	Liu et al. 2026	GitHub
Aristotle	aristotle	—	—	Achim et al. 2025	—

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.

Benchmark	DATASET	Toolchain	Paper	Source
Examples	EXAMPLES	v4.28.0	—	docs
PutnamBench	PUTNAM	v4.27.0	Tsoukalas et al. 2024	trishullab/PutnamBench
FATE-H	FATE_H	v4.28.0	Jiang et al. 2025	frenzymath/FATE-H
FATE-M	FATE_M	v4.28.0	Jiang et al. 2025	frenzymath/FATE-M
FATE-X	FATE_X	v4.28.0	Jiang et al. 2025	frenzymath/FATE-X

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