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.