| name | proof-contract |
| description | How to write a proof contract — the prompt-as-contract technique for open mathematical problems. Use when drafting or reviewing a contract that defines exactly what counts as solving a problem, before any proving starts. |
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
- 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).
- 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).
- 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.
- 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.
- 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.
- 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.
- 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).
- 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.
- 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
- Research the canonical statement and known partial results (allowed at this stage).
- 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.
- Fill 5–7 from the problem's structure; fill 8's portfolio from genuinely different
mathematical ideas, not variations of one.
- Self-audit: for each section ask "could a wrong proof slip past this wording?"
- 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.
