Installation

Install the package

open-atp targets Python 3.12+. Install it from source with uv (recommended for development):

git clone https://github.com/henryrobbins/open-atp.git
cd open-atp
uv sync

or with pip:

pip install open-atp

Quickstart

This quickstart compiles and checks a complete lake project in a local Docker sandbox via the shared Verifier. It requires:

• Docker installed and the open-atp:latest image built (see Docker).

• A complete lake project — a directory carrying its own lean-toolchain and lake-manifest.json — whose toolchain matches the image’s pin (lean_toolchain).

from open_atp.lean import LeanProject
from open_atp.verify import docker_verifier

report = docker_verifier().verify(LeanProject("path/to/lake/project"))
print(report.verified, report.sorry_free, report.axioms)

To go further than verification and actually fill the sorrys, hand a project to a prover. See Provers for the prover catalogue and Running a prover for an end-to-end walkthrough.

Note

The input contract is a full lake project. The verifier rejects projects whose pinned toolchain does not match the sandbox image (ToolchainMismatch) rather than failing deep in a build.