lean

The Lean input contract: the project to complete, the task describing what to fill, and the staging helper. A project is a full lake project carrying its own lean-toolchain and lake-manifest.json.

class open_atp.lean.LeanProject(root)

A complete lake project on disk.

Parameters:

root:

Directory containing lakefile.toml (or lakefile.lean), lean-toolchain, and lake-manifest.json.

Examples

Point LeanProject at a lake project directory and inspect it (here a minimal project is written to a temp dir to keep the example self-contained):

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.lean import LeanProject
>>> root = Path(tempfile.mkdtemp())
>>> _ = (root / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (root / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> _ = (root / "Demo.lean").write_text("theorem t : True := by sorry\n")
>>> project = LeanProject(root)
>>> project.lean_toolchain
'leanprover/lean4:v4.31.0'
>>> [p.name for p in project.lean_files()]
['Demo.lean']
>>> [p.name for p in project.files_with_sorry()]
['Demo.lean']

files_with_sorry()

Lean files that contain a sorry token (cheap textual scan).

lean_files()

All .lean source files, excluding build artifacts under .lake.

property lean_toolchain

The pinned toolchain, e.g. leanprover/lean4:v4.31.0.

property mathlib_rev

The pinned Mathlib revision from lake-manifest.json, if present.

Prefers the human-declared inputRev (e.g. v4.28.0) so it is comparable to an Image’s declared mathlib_rev, falling back to the resolved git rev (a commit SHA) when no inputRev is recorded.

root

class open_atp.lean.ProofTask(project, targets=(), instructions=None, metadata=<factory>)

A unit of work: complete the sorrys in project.

Parameters:

project:

The lake project to complete.

targets:

Optional explicit list of files (relative to project.root) to focus on. When empty, every file containing sorry is fair game.

instructions:

Optional natural-language guidance forwarded to provers that accept a prompt (e.g. Aristotle, or the agent system prompt).

instructions = None

metadata

project

resolved_targets()

targets = ()

exception open_atp.lean.ToolchainMismatch

Raised when an uploaded project’s toolchain does not match the image’s pin.

open_atp.lean.stage_files(files, dest, *, skeleton=PosixPath('/home/docs/checkouts/readthedocs.org/user_builds/open-atp/envs/latest/lib/python3.12/images/lean'))

Stage bare .lean files into the default Mathlib skeleton -> a project.

Convenience for the “upload one or more ``.lean`` files” contract: copies the skeleton’s lakefile.toml + lean-toolchain into dest and drops the files at its root. Limitation: this only works for the pinned toolchain/deps the skeleton (and the baked image) provide – a file needing a different Mathlib revision or extra deps must arrive as a full lake project instead.

Examples

Stage a bare .lean file into a skeleton to get a complete LeanProject (here a minimal skeleton is written to a temp dir; in practice skeleton defaults to the baked image’s SKELETON_DIR):

>>> import tempfile
>>> from pathlib import Path
>>> from open_atp.lean import stage_files
>>> skeleton = Path(tempfile.mkdtemp())
>>> _ = (skeleton / "lakefile.toml").write_text('name = "demo"\n')
>>> _ = (skeleton / "lean-toolchain").write_text("leanprover/lean4:v4.31.0\n")
>>> bare = Path(tempfile.mkdtemp()) / "Bare.lean"
>>> _ = bare.write_text("theorem t : True := by sorry\n")
>>> dest = Path(tempfile.mkdtemp()) / "project"
>>> project = stage_files([bare], dest, skeleton=skeleton)
>>> project.lean_toolchain
'leanprover/lean4:v4.31.0'
>>> [p.name for p in project.lean_files()]
['Bare.lean']

Staging input

A full lake project on disk is just LeanProject(Path(path)). stage_files() stages one or more bare .lean files into the pinned Mathlib skeleton.

Image defaults

The constants describing the baked sandbox image (the contract the verifier enforces).

open_atp.images.DEFAULT_IMAGE = Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0')

The image built from images/Dockerfile – all default pins.

class open_atp.images.Image(name='open-atp:latest', lean_toolchain='leanprover/lean4:v4.28.0', mathlib_rev='v4.28.0')

A sandbox image: its container tag and the Lean pins baked into it.

Carried by a BackendConfig and used by the Verifier as the compatibility contract: a project must match lean_toolchain (and, when it locks one, mathlib_rev) or it is rejected before any compute is spent.

Attributes:

namestr

Container image tag carrying Lean + Mathlib that the sandbox runs. Default open-atp:latest (the tag produced by docker build -t open-atp:latest images/).

lean_toolchainstr

Lean toolchain baked into the image (see images/lean/lean-toolchain); projects must pin it or the verifier rejects them. Default leanprover/lean4:v4.28.0.

mathlib_revstr

Mathlib revision whose olean cache is pre-baked, matching the declared pin in images/lean/lakefile.toml. Default v4.28.0.

lean_toolchain = 'leanprover/lean4:v4.28.0'

mathlib_rev = 'v4.28.0'

name = 'open-atp:latest'