# Research Loop

> How to run the portfolio research loop for open problems — route ledgers, explorer independence, blocked-route discipline, computation-as-evidence, adversarial audit cycles, and honest exits. Use when orchestrating or resuming a /prove run.

- Skill: `meleantonio/research-loop` (Agent Skill)
- Install (CLI): `npx skillmds@latest add meleantonio/research-loop`
- Raw SKILL.md: https://api.skillmd.com/api/skills/meleantonio/research-loop/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Security
- Author: meleantonio (https://skillmd.com/u/meleantonio)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/meleantonio/research-loop

---


# Running the research loop

The loop that produced Wang's six Erdős resolutions:

    attempt → failure → diagnosis → new approach → proof draft → adversarial audit → repair

Successful runs took 6–32 hours each, with roughly half of attempted problems never
resolving. The loop's design goal is symmetric: make it hard for a correct proof to be
lost AND for an incorrect proof to survive.

## The route ledger (`problems/<id>/routes.md`)

One table row per approach FAMILY — grouped by mathematical idea, not wording:

| id | family | status | artifacts | blocking gap |
|----|--------|--------|-----------|--------------|

Statuses: `active`, `blocked` (stalled at a theorem-strength missing lemma — record the
exact lemma), `refuted` (counterexample or FATAL audit — record it), `merged`.

Ledger discipline:
- Reopen a `blocked` route only for a materially new mechanism (new invariant,
  construction, estimate, certificate) — never for optimism or crowding.
- Anti-dominance: a route is not "nearly done" because it predicts a plausible constant,
  matches numerics, or gives an elegant reduction. Reduction to an unproved principle of
  comparable strength = no progress; the ledger entry must say so.
- Keep incompatible routes (including both resolution directions) alive until one side
  is rigorously ruled out.
- Failed routes are data: harvest each failure into next round's directives.

## Round structure

1. **Explore** — parallel explorers, one route each. Each gets ONLY the contract + its
   own route's notes. Do not reveal other routes or the favored approach: independent
   agents converging on the same idea is signal; anchored agents converging is noise.
   Artifacts required (lemma, construction, estimate, encoding, counterexample); status
   reports rejected.
2. **Compute** — parallel experiments: small cases, encodings (SAT/ILP/exact cover),
   extremal searches, counterexample hunts against this round's proposed lemmas.
   Everything labeled `certificate | evidence | conjecture | counterexample`; evidence
   never upgrades itself to proof.
3. **Chair pass** — update ledger, kill/spawn/redirect routes, decide which claims are
   draft-ready.
4. **Draft** — full proof draft: every lemma stated and proved, dependency structure
   explicit, no forward references.
5. **Audit** — FRESH adversarial auditor per round; inputs are contract + draft only
   (discovery notes would anchor the auditor). Verdicts: `FATAL` → refuted; `GAP` →
   blocked with exact lemma; `REPAIRABLE` → fix and re-audit fresh; `SOUND` → require a
   second independent fresh audit before promoting.
6. **Diagnose & relaunch** — convert failures into new families and sharpened lemma
   targets. Do not stop because a wave failed.

## Exits (only two are honest)

- **Candidate resolution**: two independent fresh audits return `SOUND`. Announce as a
  CANDIDATE — never "solved" — then writeup, exact-arithmetic verifier, Lean
  formalization where feasible, human review, and community-norm-respecting disclosure.
- **Failure report**: strongest rigorously proved statements + full ledger + exact
  remaining gaps. This is a respectable output; a dressed-up partial result is not.

## Budgeting

Expect hours per problem, not minutes; ask the user for a time/compute budget up front
and report ledger state at round boundaries. Long-running harnesses that retain full
context and can read/write local files are the right substrate — keep all state on disk
so a run can resume after interruption.