open-atp 0.1.1

Open Automated Theorem Proving: upload Lean files with sorrys, get verified completed proofs across multiple proving backends.

OpenATP (Open Automated Theorem Proving) runs Lean files containing sorry through leading proof-synthesis backends and returns verified completed proofs with metadata (verification status, cost, duration). Every prover — including hosted ones like Aristotle — funnels its output through one shared Verifier that compiles the candidate in a Lean+Mathlib sandbox and checks that it compiles, is sorry-free, and is axiom-clean. See the documentation for details.

Installation

pip install open-atp

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

open-atp build-image

Each harness has its own authentication requirements, and the hosted provers need their own API keys. See Installation for more details.

Quickstart

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

open-atp solve path/to/project --provers agent --backend docker

Or programmatically, here on a bundled example:

import tempfile

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

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

result = prover.prove(task, tempfile.mkdtemp())
print(result.success)

Available provers

Each name is accepted by the --provers CLI flag and the prover registry. The agentic provers run a coding-agent harness (staged into the sandbox) sharing lean-lsp-mcp; the shared Verifier does the final check regardless of which tool generated the proof.

Prover	Backing tool	Source / website
aristotle	Harmonic Aristotle (hosted)	harmonic.fun · aristotlelib
agent	Claude Code (default)	anthropics/claude-code
codex	OpenAI Codex CLI	openai/codex
opencode	opencode	sst/opencode
axprover	ax-prover (LangGraph Lean agent)	Axiomatic-AI/ax-prover-base (fork)
numina	Numina skills/prompts on Claude Code	vendor/numina/VENDOR.md
vibe	Mistral Vibe lean scaffold	mistralai/mistral-vibe

Both DockerBackend and ModalBackend run the provers and the shared Verifier end-to-end against the Mathlib image; pick one with --backend, or split generation from the cheap verify with --agent-backend.

Development

See AGENTS.md for development information.

License

MIT