Prove2Me_workspace boundary

Type: agentic-system-analyses/types/agentic-system-boundary.md

Boundary and evidence

This run examines the shipped agent skill, persistent workspace conventions, solver and captain procedures, independent statement read-back instructions, and full-project upload helpers. Its intended use is to explain how this artifact directs an external model-driven agent to discover, formalize, verify, publish, revisit and reuse mathematical work. It does not review the entire Prove2me service. The target class is workflow, not an enclosing runtime: the repository supplies agent instructions and two Lean extraction programs, while the agent's harness supplies execution and model calls. SRC-1, README.md, SKILL.md, references/mission_solver.md, references/mission_captain.md, references/mission_auditor.md.

This repository contains both the agent skill (SKILL.md + references/) and the working workspace agents operate in. --- README.md

The boundary kind is complete artifact, partial loop. All tracked repository content is eligible evidence, including shipped drivers and consumers in the reference playbooks. The artifact prescribes the loop but does not supply its enclosing model runtime, platform backend, live shared library or actual agent execution traces. The repository tree and entry-point tracing established that SKILL.md routes operators to solver/captain playbooks; the solver reads earlier attempts and writes new proofs and explanations; the captain maintains proposals and milestones; and the upload playbook consumes both shipped extractors. These callers are included, not dismissed as external merely because they direct API calls. SRC-1, SKILL.md, references/mission_solver.md, references/mission_captain.md, references/upload_full_project.md.

The orchestration code (a few Python scripts: planner, generator, uploader) is ordinary engineering you write yourself — this playbook gives you the design rules and the failure modes that are expensive to rediscover. --- references/upload_full_project.md

Functional inclusions cover credential/workspace reuse, local Lean environment setup, theorem/definition mirrors, proof and reduction submissions, verdict polling, contribution publication, proposal auditing, milestone maintenance, discussions/backlinks, and extraction-driven project conversion. The retained-state consumption paths matter: the solver is instructed to read milestone history, discussions, backlinks and prior submissions before attempting a target; the upload procedure prescribes a resumable uploader state file. These are workflow contracts, not inspected backend persistence or a shipped uploader implementation. SRC-1, references/setup.md, references/lean-setup.md, references/mission_solver.md, references/communicate.md, references/upload_full_project.md.

• Before attempting an open milestone, read its edit history (GET /milestones/:id/history) — an event that removed or replaced a theorem_id marks a rejected formalization path, and the captain's reason tells you why. Do NOT retry an approach the captain already rejected (missions.md). --- references/mission_solver.md

The frozen evidence is solely SRC-1 at full commit 38e12f9d215cb103a0f9173ec230a614fcd93b61; the cutoff is 2026-10-14, the supplied run date. HEAD was checked against that pin, and the tracked tree and working-tree status were inspected read-only. The overall evidence tier is doc-grounded because the agent loop and service contracts are instructions, not an implemented agent controller. The Lean helper programs separately support implementation-level findings about extraction. Their presence does not establish execution of the whole workflow. SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean.

Repository coverage and initial inspection

This table records eligibility and initial inspection, not a whole-system coverage claim. No tracked top-level path is deliberately excluded. Files listed as not yet read remain available at the same pin; they are not access gaps and cannot yet support detailed findings.

External dependencies and prevented conclusions

• Prove2me API and website: authentication, job queues, publication, persistent library/discussions/history, verification verdicts, reduction resolution and human/moderator launch actions are documented interfaces. Their backend implementation and live state are not in the frozen source. This prevents claims that their enforcement, persistence, isolation or automatic resolution were independently verified. SRC-1, references/setup.md, references/prove.md, references/mission_captain.md, references/communicate.md.
• Enclosing agent harness and model provider: the artifact asks the agent to execute commands, write orchestration code and launch blind auditors, but does not ship that runtime or its model-call policy. This prevents conclusions about scheduling, context isolation in practice, model selection, retries or actual compliance. SRC-1, references/mission_auditor.md, references/upload_full_project.md.
• Lean, Lake, Mathlib and user-supplied source projects: external toolchains and imports are prerequisites; project/environment scaffolding is instructed rather than bundled as an installed build. This prevents independent claims of successful compilation or environment equivalence. SRC-1, references/lean-setup.md, references/upload_full_project.md, examples/upload_full_project/README.md.
• Execution evidence: this job reads source only. No service was contacted, helper or smoke test executed, or agent episode reproduced. Expected example outputs and documentation may support bounded source-native accounts when inspected, not measured reliability, performance or causal effectiveness.

Source register