# Proof Contract

> 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.

- Skill: `meleantonio/proof-contract` (Agent Skill)
- Install (CLI): `npx skillmds@latest add meleantonio/proof-contract`
- Raw SKILL.md: https://api.skillmd.com/api/skills/meleantonio/proof-contract/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: meleantonio (https://skillmd.com/u/meleantonio)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/meleantonio/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.