| 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
- Assume a complete resolution exists for the purpose of the task.
- Do not assume the answer is yes or no in advance.
- Do not declare the problem “open” and stop.
- Do not treat reductions to equally hard unproved statements as progress.
- 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 writeupPROMPT.md — the prompt that drove the runAUDIT.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:
- Exactly one complete affirmative or negative resolution is proved.
- The argument survived adversarial audit (gaps repaired or routes abandoned).
- Artifacts are written to disk.
- 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.
