Prove2Me
Type: types/note.md
Evidence basis: repository instructions and two Lean source helpers at 326b972580e0640b1f3739ec7b12d2b34d8d3527, inspected 2026-09-25. Overall doc-grounded; no platform interaction or target execution was performed.
The Prove2Me workspace is a host integration for an external coding agent. Its skill and reference files prescribe theorem discovery, proof attempts, collaboration, human review and project upload. The remote platform, enclosing agent runtime and Lean kernel are outside the inspected artifact. The supplied code implements dependency and source-position extraction; the broader agent and verification workflows remain documented interfaces. Workspace, skill.
The ordinary solver reuses its local environment, reads prior statements and attempts, writes a proof, disproof or reduction, compiles locally, submits, polls and explains the result. Formal reuse permits open assumptions: a reduction importing an Open child can receive SKETCH_ACCEPTED, while the parent becomes Proved only after its children are Proved. ACCEPTED and SKETCH_ACCEPTED therefore carry different conditions. A successful local build also does not establish that the server's exact-target and import rules have passed. Verification and reductions.
Formal validity and faithful translation have separate consumers. The formal target governs proof checking. A fresh auditor receives only a draft's Lean code and produces a literal natural-language read-back; a human compares that rendering with the intended source before launch. Public proposals also pass moderation, whereas private launch bypasses that stage. Editing a draft clears confirmation and calls for a fresh read-back. These are procedural contracts, not runtime isolation or deployed checks established by the workspace. Audit and adoption, human and moderator roles.
Retained explanations, failed attempts, captain reasons and review history have explicit later consumers: solvers are told to inspect them before choosing another approach. This affords an attempt-to-lesson-to-later-solver learning route, without measured improvement. Most retrieval is requested by the solver or compiler; the captain-to-auditor handoff is prescribed identifier-based push. Deprecation withdraws a node from discovery while preserving imports and proof status, and deleting a milestone deletes its history. Curation changes availability and attention without necessarily changing formal warrant. Solver scouting, dead-end reports, deprecation.
The project-upload mode starts from existing proofs. Two shipped Lean helpers extract elaborated dependencies and source coordinates. The host must write the planner, generator and uploader. The playbook prescribes mechanical source slicing, exact upload-byte compilation, elaborated-type comparison and checkpoints that resume polling recorded job IDs. It does not supply an exactly-once recovery implementation. The checkpoint writer's unspecified transformation also leaves its classification as derived learning, rather than copied operational records, unresolved. Upload method, validation and continuation, source-position helper.
Campaigns add another distinct warrant: a moderator can attest that a goal instantiates a shared template and record its value while the goal remains Open. That acceptance is not a completed proof. Similarly, source citations, votes and explanations have different force from formal verification. Campaign attestation, review condition.
Scope
Internal documentation conflicts remain explicit: broad submission-source access wording versus private-proof restrictions; explanation-only PATCH wording versus submission deprecation; alternate task priorities; and different instructions for dropping spanless extraction rows. They do not establish a deployed privacy leak or a verified exhaustive API contract. The exact result retains both sides and their consequences.
The strongest learning finding is an afforded feedback-and-reuse route. Criticism and replacement are prescribed; improved future capacity, a revised theory of the agent's own organization and measured self-improvement remain unestablished. Backend/host implementation, candidate-linked checking and controlled recall comparisons would materially change this assessment.
Relevant Notes:
- Exact analysis result — see-also: canonical records, quotations, documentation conflicts, both lenses and normalized comparison fields.