Research Orchestration

Drive mathematical work toward the exact target. Treat the agent as capable of discovering and proving useful results; turn uncertainty into a specific proof obligation and the next useful action.

Launch or resume

Read the current brief and existing checkpoint first. Reuse proved results and known obstructions. Do not restart a closed route or repeat a successful check without a new mathematical reason. Check which tools, agent slots, and budgets the host actually provides.

For substantial research, explicitly use native subagents when available and permitted. This skill calls for delegation within the authorized mathematical task. Small steps can remain with the root agent. Preserve the host's model defaults and respect its concurrency limits; do not promise a fixed runtime or unavailable agent capacity. Native subagents are different from creating or messaging user-owned chats, which still require the user's authorization.

Research loop

1. Choose approaches that differ in their mathematical mechanism: a structural construction, an analytic estimate, an algebraic formulation, or a counterexample search, as appropriate. Keep early workers unaware of the favored route.
2. Ask each worker for an exact lemma, construction, calculation, counterexample, or identified gap. Have computational work serve a specific mathematical question.
3. Maintain a compact route registry in the existing research notes. Group routes by mechanism, record the obstruction and next attempt, and redirect effort when routes converge. Use the state examples only when establishing such notes.
4. Synthesize after independent work has exposed each route's strengths and gaps. Pursue a concrete promising step fully. Counterexamples to auxiliary lemmas are useful evidence for revising or replacing a route.
5. Obtain a focused fresh-context challenge to a candidate resolution or a new load-bearing bridge. Give the checker the actual argument and source material rather than the desired verdict. Use proof-audit for this work; agreement between agents is not formal verification.
6. Once a lemma has a complete proof with no unresolved substantive objection, use it immediately under its actual hypotheses. External review and novelty assessment are separate activities. Recheck when a new objection, changed assumption, or application outside the proved scope justifies it.

When a route stops at an unproved statement comparable to the original target, record the exact gap. Reopen it for a materially new mechanism, not a rewording or more enthusiastic summary. Preserve valuable proved consequences without treating them as resolution of the main problem.

For estimates, write the full parameter dependencies and quantifiers. Pay particular attention to fixed versus growing support, local versus uniform bounds, almost-everywhere versus everywhere, and detecting an exceptional object versus excluding it. Ask what unconditionally improved bound or construction the next round will deliver.

Progress and interruption

Communicate concrete achievements positively: what is proved or discovered, why it matters, and what it enables next. Use research-momentum only when a dedicated communication or reinforcement task is needed.

Continue through failed attempts while a useful next action remains within scope and budget. Honor a pause or closeout request immediately; preserve the state and finish only the bounded work requested. Follow the host's goal lifecycle rules. Neither an interruption nor an excellent partial theorem completes a still-unresolved main goal.

Formalization is optional unless requested or required by the actual task. Numerical certificates are appropriate for finite claims whose proof uses computation; analytic theorems need mathematical arguments, not repeated software checks.

When a requested or specifically useful formalization targets a decisive lemma, hand off only that bounded step to lean-formalization. Use lean-verification for formal completion claims. Keep analytical and formal status separate; continue using complete analytical results while formal library or tooling issues are resolved.