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

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

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.