Craft Proof Prompt

Craft Proof Prompt

Implement the second secret of the Wang/Erdős workflow: prompt construction inspired by OpenAI's Cycle Double Cover (CDC) prompt.

Goal

Produce a problem-specific agent prompt that defines exactly what counts as solving the problem and how the multi-agent search must behave.

Inputs

• Exact problem statement (from user or PROBLEM.md)
• Optional: example successful prompts (style references)
• Optional: known partial results, domain traps

Process

1. Read the statement carefully. Do not change mathematical content.
2. Fill every section of the template below.
3. Self-check: quote the original claim next to your restatement; they must match in meaning.
4. Write the result to problems/<slug>/PROMPT.md (or output it if no workspace).

Required prompt structure

Use this skeleton (adapt bullets to the problem; do not leave placeholders):

# Problem-specific proof prompt

## Definitions
[Define every object appearing in the statement with mathematical precision.
Include edge cases: empty structures, disconnected cases, multiplicity, etc.]

## Exact claim to resolve
[Restate the open problem verbatim in meaning.]

## What complete resolution means
A complete solution must prove **exactly one** of the following (edit to fit):

### Affirmative resolution
[Spell out the theorem to be proved — no extra assumptions.]

### Negative resolution
[Spell out the disproof / counterexample class / non-existence certificate required.]

Assume for purposes of this task that a complete resolution exists, but do **not**
assume in advance that the answer is affirmative or negative (unless the user
specified only one direction).

## Partial progress that does NOT count
List items that are insufficient, for example:
- Special cases only (restricted families, asymptotic density zero sets, etc.)
- Weaker bounds that do not settle the claim
- Reductions to another unproved statement of comparable strength
- Numerical evidence without a rigorous limit argument
- Conditional proofs under major open conjectures
- Modified problems (relaxed hypotheses, stronger conclusions smuggled in)
[Add problem-specific non-counting results.]

## Problem-specific traps and edge cases
[Enumerate definitional traps, common false lemmas, uniformity issues,
circular reductions, off-by-one / empty cases, etc.]

## Allowed background
Standard proved theorems in [relevant fields] may be used if stated accurately
with all hypotheses. Public search may be used only for ordinary background
or standard named theorems, **not** to retrieve a solution to this exact problem.

## Multi-agent search heuristics
Use multi-agent search aggressively and dynamically. Do not use a fixed
assignment such as "N agents for strategy X." Manage the search as follows:

- Begin with a genuinely diverse portfolio of approaches (different formulations,
  invariants, reductions, constructions, computational checks).
- Do not tell most agents the currently favored approach in early rounds.
- Maintain an explicit registry of approach families (group by mathematical idea).
- If many agents converge to one family, redirect some toward underexplored formulations.
- Do not allow one approach to dominate merely because of elegant reductions.
- A route that ends at a lemma equivalent in strength to the original problem
  is not close to completion unless it supplies a genuinely new proof of that lemma.
- When an approach stalls at a theorem-strength missing lemma, mark the route blocked.
  Reopen only if someone proposes a materially new mechanism, invariant, or construction.
- Keep several incompatible proof routes alive through multiple rounds.
- Cross-pollinate only after independent agents have developed ideas far enough
  to expose real strengths and gaps.
- Search aggressively for counterexamples to proposed lemmas.
- Use adversarial agents throughout: every candidate proof must be challenged
  against the traps list and the exact claim.
- Require concrete lemmas, constructions, equations, algorithms, code outputs,
  or counterexamples. Reject status reports, vague optimism, and "routine" claims
  for unproved global statements.
- The root agent should repeatedly synthesize, challenge, redirect, and launch new rounds.
  Do not stop after the first wave fails.

## Return policy
Return **only** when a complete resolution has been found **and** survives
adversarial audit. Do not return a reduction, partial result, isolated missing
lemma, "best effort" summary, or explanation of why the problem is difficult
as if it were a solution.

If stopped incomplete, report only the strongest rigorously proved derivation
and its exact remaining gap.

Do not return merely because current approaches fail. Continue launching new
rounds and searching for fresh formulations.

Style transfer (when user provides example prompts)

If the user pastes successful prompts (e.g. from an Erdős run):

1. Extract structural patterns (success criteria, non-counting lists, trap lists, multi-agent section).
2. Generate a new problem-specific prompt in the same style.
3. Verify the original mathematical statement is preserved exactly.
4. Do not copy irrelevant traps from another problem.

Quality checklist (before finishing)

• Definitions cover all symbols in the claim
• Affirmative and/or negative success criteria are unambiguous
• Non-counting list is long enough to prevent false "wins"
• Traps are specific to this problem
• Multi-agent heuristics are included
• Return policy forbids partial results as solutions
• Statement matches source (no silent strengthening/weakening)

References

• references/prompt-template.md
• OpenAI CDC prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf