proof-contract

# Writing proof contracts A proof contract turns "please solve X" into a specification a proof can be audited against. The technique (from Wang's Erdős runs, after OpenAI's cycle-double-cover experiment): **the prompt defines exactly what counts as solving the problem**, so near-misses cannot be reported as success. The full template is in `templates/proof-contract.md` (nine sections). This skill is the drafting guide. ## Why each section exists 1. **Precise restatement** — most wrong "solutions" solve a slightly different problem. Defining every symbol and resolving every ambiguity of the informal statement removes the wiggle room. Also state what is NOT being asked (neighboring quantities). 2. **Resolution criteria** — state the affirmative AND negative resolutions, each with equivalent reformulations, without presupposing direction. A disproof has its own proof obligations (nonconvergence must be proved, not just a limit not found). 3. **Established background** — known results with their exact quantifier structure, plus an explicit "does not imply" paragraph. Example of the trap this kills: treating a known order-of-magnitude bound `f(n) ≍ g(n)` as if it implied an asymptotic constant exists. 4. **Insufficient results** — the firewall. Enumerate every near-miss: reproving known results; bounds with gap between constants; unspecified constants; subsequences; almost-all; restricted families without a WLOG proof; numerics/heuristics; conditional results; finite ranges; modified problems (list the specific tempting modifications); uncontrolled relaxations; comparable-strength reductions. Longer is better; Wang's lists ran 15–20 items. 5. **Reformulation invariants** — translations (to optimization, graphs, valuations...) are where constraints silently vanish. List what must survive: distinctness, strict inequalities, exact identities, the true objective, quantifier order. 6. **Problem-specific traps** — the adversarial auditor's checklist. Mine four sources: edge cases of the definitions; classic wrong assumptions for the problem type (coprimality, extremizer symmetry/uniqueness/stability); quantitative traps (error terms too weak for the target term, floor functions, integrality gaps); circularity risks of each known reformulation. 7. **Allowed tools** — standard proved theorems, stated accurately, applied with all hypotheses and uniformity — plus the search policy (background only; never the target problem, its status, or prior attempts). 8. **Search directives** — portfolio management for the run: 10–20 concrete approach families for THIS problem; independence of explorers; a route registry; the anti-dominance rule; blocked-route discipline; both resolution directions kept alive; computational and adversarial agents throughout; artifacts required. 9. **Exit criteria** — the two honest exits only: complete resolution surviving audit, or explicit failure report (strongest proved statements + exact gaps). Forbid "best effort" summaries and difficulty essays presented as results. ## Drafting procedure 1. Research the canonical statement and known partial results (allowed at this stage). 2. Fill sections 1–3, then RED-TEAM section 2: ask "what could a strong model return that looks like success but is not?" — every answer becomes a section 4 bullet. 3. Fill 5–7 from the problem's structure; fill 8's portfolio from genuinely different mathematical ideas, not variations of one. 4. Self-audit: for each section ask "could a wrong proof slip past this wording?" 5. Have a second reader (human or fresh agent) attack the contract before the run. ## Quality bar A good contract is long (Wang's ran 80–230 lines), boring, and pedantic — that is the point. Every hour spent here is repaid the first time an audit catches a near-miss by pointing at a bullet you wrote in advance.