Prove Sop

Prove SOP

When the user asks for a statistical proof ("prove X", "show that Y holds", "give a rigorous derivation"), or when a proposition node sits without a verified proof:

1. Memory lookup: call mcp__memory__match_signatures with the proposition text and domain="proof". If similar past proof errors exist, read them first before drafting.
2. Capture the proposition: if not already in the graph, call mcp__prove__propose_proposition to register it. Pass parent_id to a related question or hypothesis node so empirical and theoretical work share one tree (architecture.md §13).
3. Skeleton retrieval: call mcp__prove__retrieve_skeletons with lexical and semantic keywords you extracted from the proposition. If fewer than 3 candidates rank above similarity 0.4, ingest more material via mcp__prove__ingest_proof_corpus first or fall back to a from-scratch outline.
4. Skeleton tournament: from the retrieved candidates plus 2-3 of your own outline drafts, register them as siblings via mcp__prove__propose_proof_skeleton. Run $bt-tournament to BT-rank them; the proof-trunk leaderboard is mcp__memory__get_bt_leaderboard(kind="proof_skeleton"). Stop when the top-2 LCB / UCB intervals separate or 3 comparisons cover every candidate.
5. Draft generation: pick the BT winner. Read the proposition plus the selected skeleton, assemble the drafting prompt inline, and generate the LaTeX draft yourself (do not spawn a sub-agent for this). Persist it via mcp__prove__register_proof_draft. At this branch point (choosing one skeleton over the others), optionally call mcp__cockpit__narrate("why this skeleton") so the cockpit reflects the decision (v5.0; optional).
6. Segment + diagnose: split the draft into minimal logical units (~3-12 snippets per page; one per non-trivial step). Call mcp__prove__segment_proof(draft_id, snippets) -- this opens a fresh diagnostic manifest. For each snippet, call mcp__prove__diagnose_snippet to get historical proof-error candidates, decide is_flawed, and call mcp__prove__register_diagnosis. After all snippets are recorded, call mcp__prove__finalize_manifest.
7. Correction (only if status='open'): call mcp__prove__compose_correction_prompt to build the global-fix prompt; generate the corrected LaTeX inline; call mcp__prove__apply_correction. The new draft is itself segmentable -- if you suspect more flaws, loop back to step 6 on the new draft_id. Before applying a global correction (a non-trivial decision among possible fixes), optionally call mcp__cockpit__narrate("...") so the activity pane shows the reasoning (v5.0; optional).
8. Empirical companion (optional, recommended for theorems with concrete constants): if the proof contains a numeric constant you only conjecture, hand off to the empirical trunk via $preregister. Lock metric, threshold, direction. The reviewer will later cross-link the theorem and the preregistration.
9. Lean reinsurance (optional): when a key lemma is small + closed (single-page, mathlib-friendly), call mcp__prove__triage_for_formalization. If eligible=True, request a wallclock budget from the budgeter agent for long attempts (see [prover.md § Budget](../../agents/prover.md)); low-cost checks may proceed with an audit warning when no budget is configured. Then spawn the prover subagent. A successful lean_verify attaches as the strongest possible evidence; a failure feeds the cross-domain failure ledger via mcp__memory__record_failure(domain="proof").
10. Reviewer: when the manuscript is ready to ship, the reviewer agent's proof checklist (P5) demands either a manifest.status='empty' plus a Lean verification, or an explicit unverified flag. Plan accordingly.

Guardrails

• BT comparisons forbid cross-kind matches; do not use update_bt_rating between a hypothesis and a proof_skeleton. Use parallel tournaments (architecture.md §13). Stop a skeleton tournament when the top-2 LCB / UCB intervals separate, or when every candidate has participated in at least one comparison.
• mcp__prove__diagnose_snippet is read-only; you must explicitly register_diagnosis for the entry to land in the manifest. This is intentional: the LLM judgment lives in the agent loop, not the MCP tool.
• A manifest only finalises once. To re-segment a corrected draft, call segment_proof on the new draft_id -- this opens a fresh manifest. Old manifests stay around as audit history.
• Lean failures are not blockers. The proof trunk's first-class output is the NL draft; Lean is reinsurance.
• Lean attempts ≥ 5 minutes should go through the budgeter agent (prover.md § Budget). Missing budget context is an audit warning, not a reason to discard the NL proof.

Cross-references

• Tool layering doctrine: [ADR 0007](../../docs/adr/0007-tools-skills-hooks-layering.md)
• Two-trunk architecture: [ADR 0008](../../docs/adr/0008-two-trunk-domain-architecture.md)
• Cooperation interfaces: [architecture.md §13](../../docs/architecture.md#13-core-vs-domain-trunks-v40)
• Empirical companion gate: $preregister
• Skeleton ranking: $bt-tournament

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: whenpoem
• Source: whenpoem/aiscientist
• License: MIT

Install and usage instructions live in the source repository linked above.