--- name: prove-protocol description: Multi-agent protocol for proving or refuting mathematical statements. Use when trying to prove a mathematical statement with agents, when a claimed lemma keeps dying under scrutiny, or when the true statement itself is still unknown (theory-finding regime). --- # prove-protocol — the full proving playbook ## 0. The discipline, and why it is shaped like this **Within this protocol, no mathematical claim is graded closed on agreement. It is graded VERIFIED-CLOSED only when an agent assigned to refute it — armed with executed exact arithmetic — has failed, and when a second agent who authored nothing has rebuilt the chain from the spec alone, reproducing every pre-registered value with fresh code.** This is a working standard for agent output, not a substitute for a refereed or formally verified proof. Everything below is machinery for manufacturing those two events on purpose. The paranoia is calibrated to three observations from practice and from the literature (Sources, below): 1. **Agreement is free.** Provers built on the same or similarly trained models share blind spots and converge on the same form — including the same wrong form. Consensus measures correlation of priors, not truth. Independence must be forced structurally (separate contexts, forbidden cross-reading, named-distinct routes), never requested in a prompt. 2. **Self-review approves its own bugs.** The reasoning that produced a flawed step is the same reasoning that re-reads it and finds it convincing. 3. **Talk is a null instrument.** Natural-language-only critique ("step 7 seems under-justified") does not move a proof's state — a measured null (the intrinsic self-correction null measured by Huang, Chen, Mishra, Zheng, Yu, Song and Zhou, arXiv:2310.01798, ICLR 2024). The only signal that cannot be socially generated is an executed exact computation at a hostile instance; every check in this protocol bottoms out in a script that ran. Two regimes. Know which one you are in before spending tokens: - **REGIME 1 — the statement is known**: run the pipeline in §1 (target-pin → adversary-first hunt → prover/skeptic core → forced-diversity provers → fresh-context cross-verify → interface trace). - **REGIME 2 — the statement is UNKNOWN or keeps dying**: theory-finding (§4). The failure smell: you pin formulation after formulation and a competent adversary kills each within hours. A consistent pattern: target reshapings come from adversaries, essentially never from provers — provers do not find theorems; searchers and adversaries do. ## 1. The pipeline core (REGIME 1) 0. **ADVERSARY FIRST (X0)** — reliably the highest-value step per token spent. Before any proving run, spend one run hunting the exact witness that makes the claim FALSE (in-regime, exact-arithmetic witness). Ladder discipline: shift the target ONLY on a certified fire (exact witness, inside the claimed regime); a NO-FIRE changes nothing. A certified kill is constructive — with pre-registered alternative forms (see step 1), the kill licenses the surviving form instead of ending the run. *Micro-example of the X0 posture.* Claim: "over the whole family, the quantity is minimized at the symmetric configuration." The adversary does not read the heuristic argument; it writes a short exact enumerator over the family's smallest members and aims it where symmetry arguments die — degenerate members, boundary parameters, the smallest asymmetric instance. A minimizer that moves at a degenerate member is a certified kill, and the witness names the repair (exclude the degenerate class, or weaken to non-strict). One agent-run; it often saves ten. 1. **TARGET-PIN as a shared SPEC**: one spec file every prover reads, containing (a) the statement/hole verbatim with source citations; (b) a MAY-ASSUME list (granted lemmas WITH their stated hypotheses) and a MUST-NOT-ASSUME list (the thing being proven); (c) licensed alternative delivery forms WITH acceptance criteria ("closes the consuming target at the printed exponents; constants may be flagged, exponents may not move"); (d) an exact test instance T1 — pre-registered rational/integer values plus named FAIL conditions ("a route whose T1 prediction fails is DEAD"); (e) an erratum channel — specs contain bugs (independent arms have repeatedly falsified claims that turned out to be bugs in the spec itself, not the mathematics), so the spec must be correctable without invalidating prover runs already in flight. Pre-register which outcome changes what. The pin agent and the X0 adversary agent are SEPARATE agents — merging them invites an output-cap death; any stage mixing statement-extraction with construction dies. 2. **SKEPTIC LOOP** (the highest-yield loop in practice): - ONE workfile is the sole shared state; pre-load the skeptic's danger list before proving starts. - The PROVER drafts the full chain with every displayed identity tied to an executed exact-arithmetic script. - A hostile fresh-context SKEPTIC does grounded spot-checks at adversarial instances and emits machine-readable bug reports — `{failing step index, exact instance, value of each side, residual}` — never an essay. Prose-only critique counts for NOTHING. - Revise against the report. Accept only after 2–3 CONSECUTIVE clean fresh-context passes. - One SNEAKY-PLANT audit, on a COPY: plant a known-false step and verify the harness CATCHES it. If the plant survives, the harness is unfalsifiable and the arm is invalid. - Any import outside MAY-ASSUME: flag it verbatim, verify it in the source, and PRE-REGISTER the downgrade path ("if ruled inadmissible → OPEN-AT step k with the rest intact"). This adversarial self-audit is what makes one-pass external verification possible. 3. **FORCED-DIVERSITY RIDER** (mandatory): ≥2 extra provers on named distinct routes, parallel fresh contexts, no cross-reading. Lesson from practice: independent arms converge unanimously on the same form with ease — and the artifact that reshapes a target tends to come only from a forced-divergent route, at any budget. The redundancy (including DNFs and failed certifiers) buys the one artifact nothing else produces. RULE: a closure without a diversity pass is graded PROVISIONAL. Cheap version: ONE skeptic chain (the proof) + ONE small tournament of 2–3 forced-distinct provers (the falsifier). 4. **FRESH-CONTEXT CROSS-VERIFY + INTERFACE TRACE** (both mandatory before VERIFIED-CLOSED). Every arm self-grades CLOSED-UNVERIFIED; nothing counts until BOTH: (a) **verify pass**: an agent that authored NOTHING re-derives the chain in its own words under hostile instructions, treats every "clearly" as a check-site, writes a FRESH independent enumerator (no code reuse) that reproduces every pre-registered exact value, and greps the load-bearing imports for circularity. Verdict: CONFIRMED / refuted, constants printed. (b) **interface ruling**: trace EVERY use-site of the delivered object in the consuming document; rule per-site whether the delivered form satisfies the consumer's STATED hypothesis (not its wording — wording is often shaped like the strong form over content the weak form covers); machine-check the composed arithmetic. This is where an alternative-form delivery gets legitimized or killed. ## 2. Failure-mode catalogue Each class is the reason a rule above exists; the vignettes describe mechanisms, not one-off accidents. - **Proof by agreement.** Provers converge on the same conclusion and the convergence is filed as verification. Mechanism: shared priors produce identical errors at any N — the agreement was determined before the first token was generated. Cure: §1.3 forced diversity plus §1.4(a); a verdict only counts from an agent that could have profited by disagreeing. - **Steps verified by their author.** The prover "double-checks" its own chain and reports all steps sound. Mechanism: the blind spot that wrote the bug re-approves it. Cure: skeptic and verifier are fresh contexts that authored nothing, always. - **The skipped hunt.** No counterexample search was run because the claim "obviously" holds — the heuristic is clean and the small cases in the prover's head work. Mechanism: obviousness is a fact about the prover's prior, not about the statement; the witness usually lives exactly where the intuition was trained not to look (degenerate and boundary instances). Cure: X0 is unconditional; it runs first even when everyone is sure. - **Talk-only skepticism.** The skeptic writes paragraphs of doubt, the prover writes paragraphs of reassurance, the workfile grows, the proof state does not move. Mechanism: language models happily co-author confidence. Cure: bug reports are machine-readable; anything without an executed instance is noise. - **The harness that cannot fail.** The verification loop passes everything — because it would pass anything. Mechanism: a checker that has never caught a planted bug has an unmeasured false-negative rate; its passes carry no information. Cure: the sneaky-plant audit — no trust before a demonstrated catch. - **The silent import.** Somewhere in step 9 the chain uses a fact outside MAY-ASSUME — often a disguised paraphrase of the target itself. Mechanism: circularity arrives dressed as a "standard fact." Cure: the verbatim import flag (§1.2) plus the verify pass's circularity grep. - **The unexecuted certificate.** The journal says "the attached script verifies this" and the script was never run to completion; one measured "certificate" failed its own pre-registered asserts when actually executed. Mechanism: writing a plausible checker and running one are different acts. Cure: script-of-record with output quoted verbatim (§3). - **Verification against wording.** An alternative-form delivery is accepted (or rejected) because it matches the consumer's sentence rather than its hypothesis. Mechanism: statements are routinely written stronger than their proofs use. Cure: the interface trace (§1.4b). - **The spec trusted as ground truth.** All arms faithfully attack a statement mis-transcribed at pin time — an index off by one, a hypothesis dropped. Mechanism: the pin has the same error rate as any other artifact. Cure: the erratum channel; treat a unanimous early kill as a possible spec bug first. - **Pin-thrash (the zombie statement).** The tenth reformulation of a repeatedly-killed claim is being pinned with fresh hope. Mechanism: the true object is usually a continuum or a mechanism, not the crisp dichotomy being re-pinned; each new pin samples the same doomed neighborhood. Cure: switch to REGIME 2 (§4). ## 3. Infrastructure rules (each learned from an agent failure) - **Skeleton-first, corrected form** (a recurring agent failure shape: bulk-read everything, then die at the output cap having planned but never written): (1) read the TARGET PIN ONLY; (2) IMMEDIATELY write the workfile skeleton, one pre-filled line per planned section; (3) read supporting files ONE AT A TIME, per section, transcribing each check into its section before opening the next file. Never hold more than one unwritten conclusion. For symbolic work: scripts write their own output files; quote ≤5-line summaries; never paste large expressions into messages. - **Never steer a running proof agent mid-run** — corrections go in relaunch prompts. Mid-run messages trigger a fatal re-planning burst. - **Disk-incremental journals with executed evidence**: the workfile is the proof state; write as you go. Transient infrastructure errors are not state changes — resume, never re-derive. A run that dies with zero bytes on disk is ungradeable: no journal = no arm. Script-of-record + output file quoted VERBATIM in the journal, so graders can replay exactly. - **AMBIGUOUS-refusal beats silent improvisation**: on a broken or ambiguous spec, halt-and-flag or redesign-with-logged-deviation (legal, gradeable). Silently improvising out-of-model parameters is a measured downgrade-to- OPEN. - **Detach all compute expected to outlive the agent's turn** (e.g. setsid/nohup or your framework's background-job facility); non-detached children die with the tool session. - **Budget honesty**: parallelism premium charged; DNFs and failed certifiers count against the arm; the metric is reusable-progress-per-token, not closure count. ## 4. THEORY-FINDING (REGIME 2 — when the statement itself is unknown) The signature of this regime: formulation after formulation gets hand-pinned, and a competent adversary kills each one within hours or days. When repeated pins die, STOP hand-guessing and search statement-space mechanically: **4a. Build the exact evaluator first** (the FunSearch / AlphaEvolve precondition: generate-and-score against an exact evaluator is the pattern behind the published machine-discovered mathematics we know of — Romera-Paredes et al., Nature 625 (2024) 468, doi:10.1038/s41586-023-06924-6; Novikov et al., arXiv:2506.13131; Georgiev, Gómez-Serrano, Tao and Wagner, arXiv:2511.02864). Assemble a LABELED CORPUS of every certified object the effort has produced (witnesses, counterexamples, controls; label quality = certified/measured/screened as an explicit field, receipt-traced). Then a FEATURE LIBRARY of computable functionals spanning the project's mechanistic vocabulary. The corpus + evaluator turn "is this candidate statement true so far?" into an exact, instant check. **4b. Forced-distinct THEORY TOURNAMENT**: 2–4 agents, no cross-reading, each LOCKED to a different organizing principle (e.g., bifurcation / symmetry-breaking; information geometry; real algebraic geometry; probabilistic / genericity). Each must deliver: the organizing picture in its lens; CANDIDATE THEOREMS fully quantified and falsifiable; an explicit object-by-object consistency table against the certified corpus; the 3 sharpest first tests; honest scoping of which certified objects fall outside its lens. Divergence between arms is data. **4c. Invariant synthesis** over the feature matrix (searchers: sparse inequality synthesis, monotone-lattice search, program search) — candidates scored by the exact evaluator, survivors handed IMMEDIATELY to an X0 adversary — never pin a synthesized statement that has not survived a dedicated falsification run. **4d. Formulation-ladder bookkeeping**: every dead formulation gets its killer recorded (witness + mechanism). The kill LIST is itself a deliverable — after enough kills it becomes a theorem-grade impossibility map, and the mechanisms usually name the surviving statement's true shape (in practice the kills typically trace to a small number of identifiable degeneracy structures). ## 5. Preconditions & priors (do not deploy blind) Published base rates without preconditions, as of the cited evaluations (Mar 2025 / Feb 2026; capabilities move quickly): 10-15% cold success (pass@1) on fresh self-contained research lemmas (LemmaBench — Peyronnet, Gloeckle and Hayat, arXiv:2602.24173); <5% average proof score on USAMO 2025 for most models evaluated at release despite strong final-answer benchmark results (Proof or Bluff — Petrov, Dekoninck, Baltadzhiev, Drencheva, Minchev, Balunović, Jovanović and Vechev, arXiv:2503.21934). Projects beat the base rate only when THREE preconditions held — check all three first: 1. **Exact-computable test instance**: T1 with exact rationals, fully enumerable in seconds — every chain and every bug falsifiable by a CAS the same hour. Absent this, the skeptic loop degenerates to natural-language self-critique (measured null). 2. **A falsifiable, pre-registered alternative**: both forms NAMED in the spec with acceptance criteria, so the adversary has a concrete statement to kill and a kill constructively licenses the survivor. Absent this, the adversary step has no target. 3. **Mature interface**: the consumers of the result already exist with stated hypotheses and a may-assume list — quantifier-completion against known consumers, not open-sea invention. Absent this, expect the ~15% prior. For REGIME 2 add: (4) a corpus of certified objects rich enough to score candidates — if you lack one, run adversary/instance-building rounds first. ## 6. What has worked in practice, and what has not WORKS (in our campaigns and in the literature cited in §5): generate-against-exact-evaluator; self-contained stuck-step consultation with CAS re-derivation; candidate-object search for analysis proofs (Lyapunov/ansatz enumeration, falsify-each-cheaply); decomposition into sublemma STATEMENTS first, split-on-verification-failure; literature retrieval (typed as retrieval, never as discovery). HAS NOT WORKED, for us or at the base rates cited in §5: autonomous end-to-end proving without a mechanical certifier; self-reported confidence; final-answer benchmarks as proving ability; natural-language-only critique. Grading: VERIFIED-CLOSED only after §1.4's two passes. Log every run — arm, budget, grade, artifacts — to a scoreboard so DNFs and failed certifiers stay visible. **Sources and acknowledgments.** This protocol was distilled from our own multi-agent proving campaigns, but its parts have antecedents we are glad to name: the verification-and-refinement loop of Huang and Yang (arXiv:2507.15855) and the practitioner techniques collected by Woodruff, Cohen-Addad et al. (arXiv:2602.03837) — problem decomposition, iterative refinement against error feedback, and the model deployed as an adversarial reviewer of existing proofs; counterexample-guided inductive synthesis (Solar-Lezama, Tancau, Bodik, Seshia and Saraswat, ASPLOS 2006) for the adversary/prover alternation; mutation testing (DeMillo, Lipton and Sayward, IEEE Computer 11(4) (1978) 34) for the planted-bug audit; Knight and Leveson's (IEEE Trans. Softw. Eng. SE-12 (1986) 96) demonstration that independently written versions fail together, which is why diversity is forced rather than requested; and, older than all of these, Lakatos's *Proofs and Refutations* (Cambridge, 1976). The exact-evaluator regime follows FunSearch and AlphaEvolve (refs in §4a); the base rates are from LemmaBench and Proof or Bluff (§5) and the self-correction null from Huang et al. (§0). ## 7. Closing checklist - [ ] Regime identified; after two dead pins, the REGIME 2 question was asked on the record. - [ ] Spec file exists: statement verbatim, MAY/MUST-NOT-ASSUME, alternative forms with acceptance criteria, exact T1 with FAIL conditions, erratum channel. - [ ] X0 adversary ran BEFORE any prover; fire/no-fire verdict recorded with witness or search transcript. - [ ] Every displayed identity tied to an executed script, output quoted verbatim in the journal. - [ ] Sneaky-plant audit run on a copy; the plant was CAUGHT. - [ ] ≥2 forced-distinct provers, no cross-reading — else graded PROVISIONAL. - [ ] Verify pass by an agent that authored nothing, fresh enumerator (zero code reuse), every pre-registered value reproduced. - [ ] Interface trace covers EVERY use-site; rulings on stated hypotheses; composed arithmetic machine-checked. - [ ] Imports outside MAY-ASSUME flagged verbatim with pre-registered downgrade paths. - [ ] Journal on disk for every arm; DNFs and failed certifiers logged, not erased. - [ ] Nothing labeled VERIFIED-CLOSED without both §1.4 passes. A wrong proof is worse than an honest OPEN.