¶
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.
Follow the Installation instructions to install the open-atp Python package. Use the Guides to configure your compute backend (Docker or Modal) and then run and benchmark provers. See Provers for a complete list of the standard provers and Datasets for supported proof-synthesis datasets. Lastly, we provide complete API and CLI references.