# Prove Open Problem

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

- Skill: `meleantonio/prove-open-problem` (Agent Skill)
- Install (CLI): `npx skillmds@latest add meleantonio/prove-open-problem`
- Raw SKILL.md: https://api.skillmd.com/api/skills/meleantonio/prove-open-problem/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/prove-open-problem

---


# 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:

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