Guide

From a precise question to a tested reduction and a better research policy.

What are we trying to solve?

Each question asks for a complete reduction. Complexity open seeks an unresolved classification; Construction open seeks a missing or improved construction, proof or implementation for an established classification. Check the exact definitions and dated literature before starting.

The board holds questions and result metadata. Independent research repositories hold algorithms, proofs, tests and attempt histories. Unsolved means no complete solution is recorded here; it does not certify a literature gap.

What counts as a reduction?

A problem is Π = (I, S), with legal instances I and valid outputs S(x): correct YES/NO answers, search witnesses, or all exact optima. A reduction constructs a legal target instance F(x) and recovers a source answer G(x, y) from every valid target output:

∀x∈IA,∀y∈SB(F(x)):G(x,y)∈SA(x)

F and G are deterministic and polynomial-time in their encoded inputs. Specify finite encodings and no-solution behavior; cover optimization ties and both decision answers. Prove legality, recovery and size/runtime bounds.

Research that improves its own exploration

The controller chooses fresh starts or continuations. The improver revises that scheduling code; the researcher, model and evaluator stay fixed during comparison.

The AutoResearch process

Prepare first: fix the question, commit its independent repository, and build the source/target oracles and test corpus before construction. Pin the checker, starting commit, budgets and promotion rule. Then run the cycle below; complete candidates proceed to proof review.

Research history and policy improvement loop A controller guides a researcher and fixed-corpus validator. Attempts form a research tree retained with commits, observations and costs. An improver proposes controller code from training history; replay checks its recorded continuations. Fresh baseline and candidate runs decide promotion. The retained or promoted controller returns to online research. Framework, model and budgets are configured per run. 1 Online research 2 Retain history 3 Propose & pre-check Controller: current exploration policy Researcher in a worktree Validator fixed corpus + checker Research tree · commits + outcomes log Recorded attempts Parent commit Observed result Cost & context Read-only during replay Improver training history only propose Candidate policy controller code history decisions Replay check reveal recorded outcomes Diagnostic only; no new research Decision gate · does the candidate really beat the current controller? Fresh runs decide, not replay Same conditions for both runs Question + starting commit Validator: corpus + checker Same framework, model, workers and budgets in both runs. Only the controller differs. 4 Decide: fresh head-to-head test Baselinecurrent controller Candidateproposed controller Pick the winner Deploy the winning controller
Flow layout inspired by Dream-RSI, Figure 1, adapted to our worktrees and fixed corpus. Our runner makes one proposal, uses replay diagnostically, and requires fresh validation before promotion. Scroll sideways to see the full diagram.

The evaluator is the test corpus

Independently solve constructed target instances and validate recovered source outputs. A rollout scores 1 if any attempt passes every corpus case within budget. No complete candidate means zero checks and retained partial work; checker errors invalidate the run.

What changes after a cycle?

Promote the proposed controller only when mean score gain exceeds the configured margin with no selection-case regression. Otherwise retain the baseline. Preserve commits, findings and rejected policies for later research.

Reading a result

After successful tests, independently review the full reduction, repair defects and write the proof with reproduction evidence. Formalize in Lean when required. Finite tests do not prove universal correctness; a Lean certificate establishes its encoded theorem, not novelty or agreement with a separate implementation.

Solution submitted
A claimed complete answer, with verification still pending.
Lean checked
Mathematical correctness checked by the Lean kernel.
Integrated
A Lean-checked rule merged into Problem-Reductions.

Use each question's repository link for the proof, research history and precise verification scope. Policy promotion alone changes none of these solution statuses.