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.