| 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
- 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.
- 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.
- Chair pass — update ledger, kill/spawn/redirect routes, decide which claims are
draft-ready.
- Draft — full proof draft: every lemma stated and proved, dependency structure
explicit, no forward references.
- 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.
- 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.
