research-loop

name	research-loop
description	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.

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.