# Prove Open Problems

> Conduct rigorous, long-horizon research on open mathematics problems through target triage, exact success contracts, diverse proof-search portfolios, computational falsification, lemma tracking, adversarial audits, and reproducible proof packaging. Use when asked to prove or disprove an open conjecture, make defensible progress on a research-level problem, select tractable open problems, stress-test a candidate proof, or organize a sustained AI-assisted mathematics research run.

- Skill: `meleantonio/prove-open-problems` (Agent Skill, multi-file: 15 files)
- Install (CLI): `npx skillmds@latest add meleantonio/prove-open-problems`
- Raw SKILL.md: https://api.skillmd.com/api/skills/meleantonio/prove-open-problems/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Research & Search
- Author: meleantonio (https://skillmd.com/u/meleantonio)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/meleantonio/prove-open-problems

---


# Prove Open Problems

Treat mathematical discovery and proof validation as separate activities.
Explore boldly, but make claims conservatively.

## Non-negotiable rules

- Preserve the problem's definitions, quantifiers, domains, asymptotics, and
  boundary cases exactly.
- Define complete proof and complete disproof criteria before searching.
- Keep computation, heuristic evidence, conditional results, and proof
  separate.
- Reject reductions that stop at an unproved statement of comparable strength.
- Seek counterexamples to every important new lemma and every structural
  assumption.
- Record failed and blocked routes so later work does not silently repeat them.
- Never report an open problem as solved unless the claim gate below passes.
- State the strongest rigorous partial result and exact remaining gap when the
  budget ends without a solution.
- Require independent expert review before presenting any research-level result
  as established mathematics.

## 1. Choose the run

Determine these parameters from the request and available context:

- **target**: one fixed problem, or a set requiring triage;
- **resolution modes**: proof, disproof, exact value, classification, or other
  exhaustive alternatives;
- **search mode**: `literature` or `blind`;
- **resource budget**: time, tool calls, compute, and parallel-agent capacity;
- **allowed tools**: web, code, CAS, SAT/SMT, proof assistants, or none;
- **deliverable**: research log, partial theorem, candidate proof, formal proof,
  paper draft, or audit.

Use `literature` mode unless the user or benchmark prohibits exact-problem
search. In literature mode, verify the statement and current status from
primary sources. In blind mode, record the restriction and do not search for
the exact problem or its solution.

If selecting among problems, read
[`references/problem-selection.md`](references/problem-selection.md) and apply
its scorecard. Prefer meaningful, sharply stated, verifiable problems that are
not obviously bottlenecked by a flagship conjecture or missing theory.

## 2. Create persistent state

For a fresh run, execute from this skill directory:

```bash
python3 scripts/init_workspace.py <research-directory> \
  --title "<problem title>" \
  --mode literature \
  --budget "<resource budget>"
```

If execution is unavailable, reproduce the structure in
`assets/research-workspace/`. Do not overwrite an existing research directory
unless the user explicitly requests it.

Maintain these artifacts throughout the run:

- `PROBLEM.md`: frozen statement, provenance, definitions, and quantifiers;
- `SUCCESS_CRITERIA.md`: acceptable resolutions, insufficient results, allowed
  assumptions, and search policy;
- `APPROACHES.md`: approach-family registry and route statuses;
- `LEMMAS.md`: dependency ledger with proof and falsification status;
- `EXPERIMENTS.md`: reproducible computational evidence;
- `SOURCES.md`: primary sources and imported theorem hypotheses;
- `PROOF.md`: current proof candidate and unresolved gaps;
- `AUDIT.md`: adversarial defects, repairs, and sign-off;
- `STATE.json`: machine-readable run and claim status.

Run `python3 scripts/validate_workspace.py <research-directory>` periodically.
Run it with `--strict` before any solution claim.
Delete each `<!-- FILL: ... -->` marker only after completing and checking that
section; strict validation treats remaining markers as unresolved work.

## 3. Freeze an exact success contract

Write the original statement verbatim or with a checked equivalence. Then make
the implicit contract explicit:

1. define every object and convention;
2. expand all quantifiers and parameter ranges;
3. enumerate mutually exhaustive resolution modes;
4. state exactly what each complete resolution must establish;
5. list tempting weaker results that do **not** count;
6. list problem-specific traps and edge cases;
7. identify allowed background theorems and required uniformity;
8. state what computation can and cannot certify; and
9. state the search mode and resource budget.

Compare the completed contract against the source statement a second time.
If they differ, repair the contract before proof search.

## 4. Build a diverse approach portfolio

Generate approaches from different mathematical families, not paraphrases of
one idea. Include both affirmative and negative routes when either could
resolve the problem. Typical families include:

- structural or minimal-counterexample induction;
- extremal, probabilistic, or entropy arguments;
- algebraic, analytic, geometric, topological, or categorical reformulations;
- duality, compactness, invariants, decompositions, or flows;
- explicit constructions and counterexample search;
- finite-model, symbolic, numeric, SAT/SMT, ILP, or proof-assistant probes.

Preserve independence in the first round. Do not tell every explorer the
currently favored idea. Register each family in `APPROACHES.md` and redirect
effort when too many routes converge prematurely.

Use these route states:

- `active`: producing concrete deductions or tests;
- `promising`: has a plausible mechanism and discharged dependencies;
- `blocked`: stops at a theorem-strength missing lemma;
- `refuted`: contradicted by proof or counterexample;
- `merged`: subsumed into another route;
- `complete-candidate`: supplies an end-to-end argument awaiting audit.

Read [`references/orchestration.md`](references/orchestration.md) when multiple
agents or isolated contexts are available. Allocate them dynamically by
evidence and underexplored families, not by a fixed quota.

## 5. Run the research loop

Repeat until the claim gate passes or the resource budget ends:

1. choose an active or underexplored family;
2. demand a concrete lemma, construction, inequality, certificate, or
   counterexample;
3. record dependencies in `LEMMAS.md`;
4. attack the weakest dependency before building on it;
5. test small cases and adversarial examples where useful;
6. diagnose each failure precisely;
7. block, refute, repair, or redirect the route;
8. cross-pollinate only after independent routes expose their real mechanisms;
9. synthesize an end-to-end proof only from discharged dependencies; and
10. launch a fresh adversarial audit.

Classify failures as definitional, false lemma, missing uniformity, circular
reduction, hidden regularity, incomplete cases, invalid theorem use, or
computational overreach. A diagnosis must change the next experiment.

Require concrete mathematical output from parallel agents. Reject vague
optimism, literature-style summaries, and claims that a central compatibility
step is “routine.”

## 6. Use tools without confusing evidence for proof

- Use code, CAS, SAT/SMT, and search to find patterns, falsify lemmas, verify
  finite certificates, and check algebra.
- Record command, environment, inputs, seed, output, and interpretation in
  `EXPERIMENTS.md`.
- Treat finite computation as evidence unless a proved reduction makes it
  exhaustive and the certificate is independently checkable.
- State every imported theorem accurately with all hypotheses and cite a
  primary source in `SOURCES.md`.
- Formalize the final argument in Lean, Coq, Isabelle, or another checker when
  practical. Formalization strengthens verification but does not repair a
  mistranslated original statement.

## 7. Audit and repair

When a route becomes `complete-candidate`, freeze that version and read
[`references/audit-checklist.md`](references/audit-checklist.md).

Use an auditor that did not author the proof when possible. Give the auditor
the frozen problem, success contract, proof, and permitted background, but not
the author's defense. Require line-specific defects, counterexamples, or
missing dependencies. Log every defect and repair in `AUDIT.md`.

After a repair, re-audit the affected lemma and every downstream step. Reopen
proof search if the repair introduces a new theorem-strength gap.

## Claim gate

Set `claim_status` to `candidate-solution` only when all of the following hold:

- the proof or disproof matches an allowed resolution exactly;
- every case and quantifier in the frozen statement is covered;
- every nonstandard lemma is proved with no circular dependency;
- every imported theorem's hypotheses are checked;
- computation is either nonessential evidence or a verified exhaustive
  certificate;
- edge cases and degenerate objects pass adversarial review;
- at least one independent audit has no unresolved substantive defect;
- `validate_workspace.py --strict` passes; and
- `STATE.json` records `proof_status: "audited"` and
  `audit_status: "passed"`.

Set `claim_status` to `solved` only after the candidate also receives either:

- an external human expert audit; or
- machine verification of the exact formalized statement, together with an
  independent check that the formal statement faithfully translates the
  original problem.

Record the validation source in `STATE.json.audit_independence`. A different
agent can support `candidate-solution`, but model agreement alone does not
establish a research theorem. If any candidate gate item fails, use `partial`,
`conditional`, or `counterexample-candidate`.

## 8. Package the outcome

For a complete candidate, deliver:

- exact theorem statement and proof source;
- dependency and audit summaries;
- reproducible code, certificates, and raw logs;
- primary-source bibliography;
- formalization or a precise formalization plan when practical; and
- an explicit request for independent expert validation.

For an incomplete run, deliver:

- strongest rigorously proved result;
- exact unresolved gap;
- refuted and blocked approaches;
- reusable computations or lemmas;
- the most informative next experiments; and
- an honest claim status.