Prove2Me_workspace synthesis
Type: agentic-system-analyses/types/agentic-system-synthesis.md
Bounded synthesis
From mathematical source to an agent-operated workspace
Prove2Me_workspace supplies instructions for external agents to formalize, prove, publish and revisit mathematics, plus two executable Lean extraction helpers. It is a workflow artifact, not an enclosing agent runtime. This account covers SRC-1, https://github.com/prove2me/Prove2Me_workspace, at commit 38e12f9d215cb103a0f9173ec230a614fcd93b61, with an analysis cutoff of 2026-10-14. The boundary is complete artifact, partial loop: the repository's procedures and helpers are included, but the model harness, Prove2me backend and live shared library are not supplied. The overall evidence is doc-grounded; helper implementation supports narrower code-grounded findings. No execution trace or causal experiment establishes end-to-end operation. The worked example supplies candidate artifacts and attributed compilation, not an inspected service acceptance episode. See the boundary and evidence, Source register and report verification.
The entry skill routes the foreground agent to solver or captain procedures; an already-proved project uses a separate upload procedure. The host supplies model calls, shell/file tools, HTTP execution and sub-agent contexts. The foreground agent owns target selection and the next action. Persistent credentials, local Lean mirrors and environment/build files support reuse of the workspace; they do not automatically enter model context. The service supplies the documented library, jobs, verdicts and histories. Neither host grants nor deployed model fixity are established. See RT-OBJ-skill, RT-CMP-agent-model and MEM-OBJ-workspace-files, SRC-1, SKILL.md, references/lean-setup.md.
Formalizing a source: testimony, comparison and publication
The representative connected workflow begins with a human's mathematical source and goal. A captain reads the source's assumptions, searches for existing declarations, and drafts missing definitions and theorem targets in dependency order. Draft storage is not verification. For each new declaration, the captain is instructed to give an independent auditor only Lean code, its preamble and the auditor procedure in a fresh context. The auditor returns a literal mathematical read-back, not a judgment of source faithfulness. The human then compares that testimony and code with the intended mathematics. This separates a model's account of what the code says from a human's decision that it says the right thing. Isolation is a host-dependent instruction, and read-back remains optional API content. See RT-RTE-proposal-audit, RT-OBJ-readback and the workflow account, SRC-1, references/mission_captain.md, references/mission_auditor.md.
Human confirmation and website submission precede the documented compile-and-publish transition. Successfully compiled items become immutable library declarations before public moderator approval. Reviewed delivers a public mission with a goal and curated milestones, not a proof of that goal. Private launch uses the same human confirmation and publication sequence but skips moderation. Direct contributions and project uploads do not inherit proposal confirmation; private-tree release separately requests human authorization. Thus neither human proposal launch nor public moderation is a universal pre-publication gate. See RT-CLM-human-gate, RT-RTE-content-publish and report verification, SRC-1, references/mission_captain.md, references/contribute.md, references/upload_full_project.md.
Correction has explicit owners. Draft edits require renewed human confirmation, and statement edits require fresh read-back. After publication, a defective statement needs a successor under a new name, updated goal/milestone links and another review round. The captain reads retained moderator reports and item flags before repairing it. Deprecation hides discovery while preserving imports and proof status; milestone unlinking does not revoke membership, and milestone deletion destroys its history. These are different recovery actions, not one rollback mechanism. See RT-RTE-proposal-audit, MEM-OBJ-proposal-reviews and MEM-OBJ-milestone-history, SRC-1, references/mission_captain.md, references/contribute.md.
Solving and retaining work: exact formal targets, conditional reductions
A solver scouts the target, source references, audits, discussions, prior submissions and milestone edit history. It mirrors the formal declaration, writes a solution, preferably compiles locally, submits to /verify, records the returned ID and polls for a terminal result. Failed immutable code is repaired through a new submission; explanation prose can be edited. The documented service checks the exact target in its environment. Local compilation is not equivalent: it may permit importing the target's own sorry-stub, which the server contract rejects. A disproof must negate the whole quantified statement. Formal checking does not certify faithful translation of the informal source. See RT-RTE-solver-proof, RT-OBJ-solution and RT-CLM-verification-boundary, SRC-1, references/prove.md, references/lean-setup.md.
A reduction may import Open child theorems as tracked assumptions and receive SKETCH_ACCEPTED. That result is conditional, not unconditional closure. The service is claimed to resolve the parent when all imported children become Proved. Separately, published Open theorem stubs are targets to solve, whereas definition files must be sorry-free. Retention and operational use can therefore precede proof. See RT-RTE-reduction-proof, EPI-OBJ-formal-statement and EPI-OBJ-definition, SRC-1, references/prove.md, references/contribute.md.
The strongest supported experience-feedback contribution is a prescribed chain from failed code, authored explanations/comments and captain rejection reasons to later solver scouting. Reasons have named later readers; parsed links chiefly locate the underlying artifacts. Requested IDs, filters, graph roots, saves and pagination select retained material. These are pull routes, not established automatic context injection; page caps are not token budgets. Retention alone does not show changed behavior or improved future capacity, and optional description histories and rating reasons lack comparable routine consumers. See MEM-RTE-discussion-feedback, MEM-RTE-solver-scouting, MEM-BAP-experience-guidance and MEM-OBJ-description-versions, SRC-1, references/communicate.md, references/discover.md, references/mission_solver.md.
Selection signals have different authority. Votes and trust influence priority, not truth; collection membership changes navigation, not Lean imports or verification. Campaign moderators attest that a numerical goal matches a shared template and foundation. An attested Open entry is still a proposed bound. latest_value selects only Proved goals by recording recency, not the best bound; preferred-value ordering is separate. See EPI-RTE-quality-signals, EPI-RTE-collection-admission, EPI-RTE-campaign-review, EPI-RTE-campaign-admission and EPI-RTE-campaign-selection, SRC-1, references/curate.md, references/collections.md, references/campaigns.md.
Uploading a proved project: implemented extraction, prescribed conversion
The upload route starts with a built, pinned project and selected theorem roots. Stage 1 extracts elaborated declaration dependencies; Stage 2 re-elaborates source files and emits declaration spans and original-position constant references. Stage 2's inspected error guard prevents normal successful fact emission after elaboration errors. Its reference surface excludes recursive self-references elaborated as locals and some generated syntax. These facts support conversion planning, not complete semantic preservation. See EPI-RTE-extraction-facts, RT-CMP-extract-decl-graph and RT-CMP-extract-sketch-info, SRC-1, scripts/extract_decl_graph.lean, scripts/extract_sketch_info.lean.
The agent must write the planner, generator and uploader. The procedure requires instance roots, careful span/namespace transformations, re-extraction after source edits, axiom checks, exact-payload compilation and original-versus-staged elaborated-type comparison. Leaves-first publication and a final zero-Open check precede proposal handoff. A state file and recorded job/submission IDs are prescribed for interrupted-run recovery, but no shipped uploader proves duplicate-free behavior across remote-success/local-recording crashes. For project transplantation, the architectural assessment is therefore stronger for fact production than for preservation, recovery or completion. See RT-RTE-project-upload, MEM-OBJ-upload-state and EPI-CLM-graph-truth, SRC-1, references/upload_full_project.md.
Independent theory-building and improvement findings
At the mathematical-product boundary, the proposal route affords localized whole propositions (condition 1), claims content-dependent admission (condition 2), claims localized criticism and replacement (condition 3), and claims retained feedback shaping later rounds (condition 4). These statuses do not establish an exercised theory builder. For direct solving, condition 1 is afforded and conditions 2 and 4 are claimed, while condition 3 remains uninspected. Reductions afford condition 1 and claim condition 2 without established criticism or iteration for conditions 3 and 4. See the separate assessments in RT-RTE-proposal-audit, RT-RTE-solver-proof and RT-RTE-reduction-proof.
Criticism retention and successor construction are the supported partial contribution; whether criticism of a consumed theory improved capacity for future action remains uninspected. Trace learning is also unresolved: the records do not identify a complete automatic recorded-trace-to-durable-derivative-to-later-consumer chain. This is neither an absence finding nor a requirement for weight updates. Reflection remains uninspected because no two-direction self-representation of the workflow is established. Autonomous theory building is inapplicable to the prescribed proposal comparison/admission boundary, which includes human and moderator internal decisions; solver autonomy remains uninspected rather than following from permission to proceed between human contacts. See RT-RTE-proposal-audit, MEM-RTE-discussion-feedback, RT-CMP-agent-model and profile verification.
For keeping workflow instructions compatible with the service across current and later workspace sessions, version mismatch can trigger a repository pull. This is a claimed behavior-changing maintenance surface, not exercised self-improvement: the records do not establish evidence shaping a specific content revision or subsequent operation causally depending on it. Product correction and agent-written conversion scripts likewise do not by themselves establish improvement of the workflow's own organization. See RT-RTE-workspace-refresh and RT-RTE-project-upload, SRC-1, SKILL.md, references/upload_full_project.md.
The assessment would change with implemented backend gates and closure logic, host-enforced auditor input isolation, a shipped converter/comparator and crash-safe uploader, or linked episodes showing source/code comparison, consequential correction and later reliance. Capacity improvement would additionally need an appropriate comparison tracing retained criticism to improved future action; exercised self-improvement would need the instruction-update evidence, live consumer and causally dependent subsequent operation. No direct source reads were needed for this synthesis.
Limitations
| Limitation | Affected SRC IDs and record citations | Inspected boundary | Conclusion prevented | Evidence that would resolve it |
|---|---|---|---|---|
| Inconsistent submission PATCH contract; carried report-verification limit | SRC-1; report limits, RT-RTE-solver-proof, RT-RTE-content-publish | references/prove.md permits only creator explanation PATCH; references/contribute.md prescribes submission deprecation with wider retirement authority |
Exact accepted backend keys and universal submission-edit permissions; immutable proof code and bounded retirement contracts remain supported | Pinned endpoint implementation and permission rules, or reconciled authoritative contracts |
| Omitted formal-target validation consumer in the partial memory-profile inventory; carried profile-verification limit | SRC-1; profile limits, RT-OBJ-solution, RT-RTE-solver-proof, EPI-OBJ-formal-statement | Accepted records identify retained target checking, separately from template/link validation | Complete consumer-level validation inventories and validation-route coverage comparisons; existing validation witnesses remain valid | A revised profile inventory explicitly classifying the formal target at solution verification |
| External service implementation and live persistence unavailable | SRC-1; boundary, RT-RTE-solver-proof, RT-RTE-reduction-proof, MEM-OBJ-library-declarations | Workspace contracts, not verifier, closure, storage or authorization code | Independently implemented or observed enforcement, closure, persistence and permissions | Frozen backend implementations and linked service events at matching versions |
| Host/provider internals and model fixity uninspected | SRC-1; RT-CMP-agent-model, RT-RTE-proposal-audit | Auditor input policy and unspecified external models | Actual context isolation, complete memory/push inventories, parameter updates and deployed model fixity | Host context construction and delivery code, model resolution records and scoped retained-state routes |
| No linked end-to-end acceptance or causal evidence | SRC-1; report verification, RT-RTE-proposal-audit, MEM-RTE-solver-scouting, RT-RTE-workspace-refresh | Instructions, helper code and source-native example candidates/reported compilation | Successful coordination, exercised acceptance, reliably detected mismatches, capacity improvement or exercised self-improvement | Provenance-linked episodes and comparisons identifying criticism, update, later consumer and outcome at the assessed horizon |
| Formal checks do not warrant informal-source equivalence | SRC-1; RT-CLM-verification-boundary, RT-OBJ-readback, EPI-OBJ-source | Exact formal targets and prescribed human comparison; external mathematical sources not separately frozen | Source truth or faithfulness of a concrete formalization from compilation/status/testimony alone | Exact source/code pairs, relevant assumptions and recorded criterion-based semantic comparison |
| Extraction has a partial reference surface and unshipped downstream conversion | SRC-1; EPI-RTE-extraction-facts, RT-RTE-project-upload | Original-position constant facts; recursive locals and generated syntax may be omitted | Complete rename coverage, semantic preservation or completed project transplant from extraction alone | Converter/comparator implementation plus performed axiom, exact-payload, type-diff and terminal-status checks |
| Recovery and publication atomicity not established | SRC-1; MEM-OBJ-upload-state, RT-RTE-project-upload, workflow account | Prescribed action recording and compile-and-publish sequence | Duplicate-free crash recovery or rollback of earlier published items on whole-submit failure | Durable admission/idempotency protocol and transaction implementation with relevant failure evidence |
| Withdrawal is scoped, not global revocation | SRC-1; RT-RTE-content-publish, MEM-OBJ-milestone-history, MEM-OBJ-mission-comments | Deprecation, unlinking, soft deletion and history deletion contracts | Guaranteed removal of all future reliance or preservation of all anti-retry history | Explicit downstream invalidation/revocation mechanisms and history retention guarantees |
| Some historical fields have no established routine consumer; trace-update provenance unresolved | SRC-1; MEM-OBJ-description-versions, MEM-OBJ-discovery-metadata, MEM-RTE-discussion-feedback, profile verification | History endpoints, optional rating reasons and authored experience contracts | Universal feedback activation, rating-to-ranking linkage or a classified automatic trace-learning/source pathway | Named later readers, actual ranking wiring and recorded inputs to automatic durable guidance production |