prove-open-problem

name

prove-open-problem

description

Attack an open mathematical problem end-to-end using the Wang/Codex Erdős workflow: select tractability, craft a problem-specific proof prompt, run a long attempt→audit→repair research loop with multi-agent search, and emit LaTeX/Python/Lean artifacts. Use when the user asks to prove, disprove, resolve, or attack an open math problem (Erdős, conjectures, research questions), or when they mention prove-that-shit / open-problem proving.

Prove an open mathematical problem

Implement the workflow popularized for attacking open Erdős-type problems with coding agents (see docs/SOURCE_THREAD.md). Deep domain expertise helps for auditing, but the agent workflow itself is procedural.

Non-negotiable posture

1. Assume a complete resolution exists for the purpose of the task.
2. Do not assume the answer is yes or no in advance.
3. Do not declare the problem “open” and stop.
4. Do not treat reductions to equally hard unproved statements as progress.
5. Partial results, heuristics, and finite computations do not count unless they complete one of the exact affirmative/negative resolutions in the prompt.

Pipeline

Execute these phases in order. Persist artifacts under problems/<id>/.

Phase 0 — Intake

• Capture the exact statement, source URL/ID (e.g. Erdős problem number), and any user constraints (time budget, Lean required, computational tools).
• If the statement is ambiguous, rewrite it precisely before continuing.

Phase 1 — Selection gate

Run select-tractable-problem (or apply its checklist inline):

• Prefer problems actively discussed by working mathematicians.
• Reject (or demote) problems that are clearly equivalent to a major named conjecture, or that AI triage rates as “requires a new theory.”
• Record the go/no-go decision in problems/<id>/STATUS.md.

If rejected, stop and propose alternatives. Do not burn a long run on a doomed instance without user confirmation.

Phase 2 — Craft the prompt

Run craft-proof-prompt to produce problems/<id>/PROMPT.md from templates/problem-specific-prompt.md.

The prompt must:

• restate the problem precisely;
• specify exactly what counts as a complete proof or disproof;
• list weaker results that do not count;
• list problem-specific traps and edge cases;
• instruct multi-agent search management (diverse routes, blocked routes, counterexample search, adversarial auditors);
• ban answering that the problem is open / searching only to check openness.

Before the long run, verify the crafted prompt preserves the original statement exactly (no silent strengthenings or weakenings).

Phase 3 — Launch the long research loop

Set the filled prompt as the goal for a long autonomous coding-agent run (Codex /goal, Cursor long agent session, Claude Code continuous task, etc.).

Recommended model posture: the strongest available reasoning model at maximum effort. Expect multi-hour runs; successful attacks in the source workflow took roughly 6–32 hours.

Loop until the principal question is resolved and survives audit:

attempt → failure → diagnosis → new approach → proof draft
  → adversarial audit → repair → (repeat)

Maintain APPROACH_REGISTRY.md:

Family	Status	Why blocked / next move
…	exploring / blocked / promising / ruled-out	…

Rules of engagement:

• Keep several incompatible routes alive (including yes and no).
• Search aggressively for counterexamples to proposed lemmas.
• Mark a route blocked if it only reduces to another unproved statement of comparable strength.
• Abandon broken ideas; do not polish a dead route.
• Require concrete lemmas/constructions/code — reject vibes.

Phase 4 — Adversarial audit

Run adversarial-proof-audit on every candidate complete proof. Prefer an independent agent/model that did not draft the proof.

No proof is done until the audit finds no substantive gaps.

Phase 5 — Package artifacts

Produce at least:

• paper.tex / DRAFT_PROOF.md — human-readable rigorous writeup
• PROMPT.md — the prompt that drove the run
• AUDIT.md — audit log and repairs
• optional experiments/*.py for computational certificates
• optional Lean formalization via formalize-proof

Completion criteria

Return to the user only when all hold:

1. Exactly one complete affirmative or negative resolution is proved.
2. The argument survived adversarial audit (gaps repaired or routes abandoned).
3. Artifacts are written to disk.
4. Remaining open follow-ups (Lean, sharper constants) are explicitly labeled as follow-ups, not as the main claim.

Anti-patterns (never do these)

• Searching the web just to confirm the problem is still open, then quitting.
• Declaring victory with a plausible constant from numerics.
• “Proof” that assumes a structural lemma equivalent to the claim.
• Single-route tunnel vision after one attractive idea appears.
• Stopping after the first failed wave of agents.