| name | agent_group_discuss |
| description | Dynamically plan a multi-agent discussion, review, or research workflow with role selection, model assignment, round control, and recovery-aware orchestration. |
| user-invocable | true |
| disable-model-invocation | true |
Agent Group Discuss
You are the orchestrator for dynamic multi-agent work.
Use this skill when the user asks in normal language for:
- a group discussion
- a panel of agents
- multiple agents to discuss something
- a multi-agent review
- a review-only request that explicitly asks for multiple agents or a panel
- a multi-agent research session
- agents with different roles or different models
If the request is review-only and does not ask for annotation, keep it in this skill for the multi-agent route; do not route it to annotated-review unless annotation is also explicitly requested.
Supporting files
Use these local support docs when relevant:
TEMPLATES.md for named review and research templatesEXECUTION.md for round topology, time estimates, and orchestration rulesMODEL_TIERS.md for the live model catalog and research-task overrideMODEL_TIERS.example.md only as a customization templateREADME.md for the short request shape
If the user requests a named template, or the task clearly matches one, open TEMPLATES.md and EXECUTION.md before running the session.
Clarification policy
If the request is missing information, ask only for the minimum needed.
Use this compact question when needed:
“Before I start: do you want discussion, review, or research? How many rounds? Any hard constraints? I can choose roles and models automatically if you want.”
If the user gives no preference, default to:
- mode: infer from the task
- rounds: 2
- roles: 3
- interaction: auto
- role/model selection: automatic
Routing to structured workflows
If the request is clearly better suited to an installed OpenProse workflow, say so briefly and ask:
“I can run this as a conversational skill or as a more structured workflow. Which do you want?”
Prefer OpenProse if the user says:
- structured workflow
- use prose
- compile the workflow
- run the workflow
- deterministic
Otherwise stay in this skill.
High-level goal
Given a task, you must:
- classify the task
- decide which roles are needed
- decide how many subagents are useful
- assign a model to each role
- choose how the subagents interact
- run the requested number of rounds
- synthesize the result
- maintain durable recovery state on disk
Required review-validate-fix loop
Use this loop for every multi-agent discussion, review, or research run:
- Review — inspect the user goal, selected template, role plan, model assignments, constraints, and prior round outputs.
- Validate — confirm the plan is OpenClaw-native, user-approved, scoped, and free of unsupported claims or copied external settings.
- Fix — adjust roles, rounds, prompts, evidence requirements, or conclusions before continuing.
- Repeat after every round and before final delivery.
For research outputs, the final synthesis must include a compact Review Findings pass and a Delivery Check. If material evidence remains unchecked, write incomplete analysis and list what remains unchecked.
When the task is about adapting another system into OpenClaw, treat external workflows as source patterns only. Do not copy external model choices, path layouts, runtime wrappers, or agent defaults unless the user explicitly asks for a compatibility experiment.
Input format
Accept either free-form text or a structured block such as:
topic:
mode: discussion | review | research | mixed
rounds:
max_agents:
interaction: auto | star | debate | panel_judge
output:
constraints:
If the user specifies rounds, obey it.
Role selection
Prefer 3 roles by default.
Use 4 or more only when the task clearly benefits.
Typical roles by mode:
Discussion
- Optimist
- Skeptic
- Pragmatist
- Judge
Review
- Correctness reviewer
- Edge-case reviewer
- Clarity reviewer
- Synthesizer
Research
- Literature scout
- Hypothesis generator
- Critic / falsifier
- Synthesizer
Model assignment
Each role gets a model and thinking level via sessions_spawn's model and thinking parameters.
Refer to MODEL_TIERS.md for the model catalog, reasoning classifications, and profiles.
Reasoning level classification
Models are classified R1–R4 by reasoning capability:
| Level | Capability | Assign to |
|---|
| R4 — expert | Multi-step proofs, formal math, adversarial reasoning | Theorem verification, PSPACE reductions, correctness critique |
| R3 — strong | Solid structured reasoning | Planning, synthesis, algorithm design, structured review |
| R2 — solid | Adequate for most tasks | Edge-case review, advocacy, specialist analysis |
| R1 — basic | Fast generation and summarization | Scouting, brainstorming, clarity review |
Profile selection
Detect the task's reasoning demands and select a profile:
| Task signal | Profile | Lead model level |
|---|
| Formal proof, theorem, correctness verification, PSPACE, NP-hard | math-heavy | R4 with extended thinking |
| Research paper review, algorithm design, critical decision | premium | R4 leads, R3 supports |
| General discussion, code review, exploration | balanced (default) | R3 leads, R2 supports |
| Quick sanity check, opinion gathering, lightweight summary | budget | R2 leads, R1 supports |
If the user specifies a profile (e.g., "use budget models"), select all models from that profile.
If the user specifies a model for a specific role (e.g., "use opus for the judge"), override that role only.
If no preference is given, auto-detect from task signals or default to balanced.
Tier assignment by role type
| Role type | Tier | Reasoning need |
|---|
| planner, judge, synthesizer, critic, correctness reviewer | STRONG_REASONER | Must reason deeply and catch subtle errors |
| advocate, specialist reviewer, edge-case reviewer | BALANCED_MODEL | Solid reasoning for specific angles |
| scout, brainstormer, pragmatist, clarity reviewer | FAST_MODEL | Speed and breadth over depth |
Record the chosen profile, per-role model, and thinking level in state.json.
Token management
Do not promise token overflow cannot happen.
Keep prompts compact and summarize prior rounds before relaying them.
If a subagent response is truncated (ends mid-sentence or hits output limit):
- Note the truncation in
state.json under notes
- Re-spawn the role with a shorter context (summarize prior rounds more aggressively)
- If re-spawn also truncates, extract what is usable and continue with a note
- Never silently discard a truncated response — always flag it in the final output
Interaction design
Choose:
If the user requests one explicitly, obey it.
Round control
If rounds is provided, obey it.
Otherwise:
- default to 2 rounds for discussion/review
- default to 2 or 3 rounds for research depending on complexity
Never exceed 5 rounds unless the user explicitly asks.
Timeouts
Per-round timeout: 10 minutes (default). If a spawned role does not respond within this window:
- Mark the role as timed out in
responses_received
- Add a note to
pending_work
- Continue the round with the responses that were received
- Do not block the entire run for one unresponsive role
Total run timeout: 30 minutes. If exceeded, write the best available synthesis from completed rounds and set status: "failed" with a note explaining what was incomplete.
Required durable state
Create a run folder under data/runs/<run_id>/.
Before spawning subagents:
- Create
data/runs/<run_id>/lock (a file containing the current timestamp). If the lock file already exists and is less than 30 minutes old, abort with an error — another run is in progress. If the lock is older than 30 minutes, remove it (stale lock) and proceed.
- Write
data/runs/<run_id>/plan.md
- Write
data/runs/<run_id>/state.json
- Show the plan to the user before executing (unless the user said "just run it")
Before each spawn batch, validate the state file against the current plan. If roles, model assignments, constraints, or expected outputs changed, fix plan.md and state.json before continuing.
After the run completes (success or failure), remove the lock file.
Plan output format
The plan.md and the user-facing plan summary must include:
## Run Plan: <run_id>
**Topic:** <topic>
**Mode:** <mode>
**Profile:** <profile>
**Interaction:** <pattern>
**Rounds:** <N>
**Estimated total time:** <X-Y minutes>
### Subagent assignments
| # | Role | Model | Reasoning | Thinking | Est. time |
|---|------|-------|-----------|----------|-----------|
| 1 | Planner | {{ MODEL_ID }} | R4 | extended | 2-4 min |
| 2 | Correctness Reviewer | {{ MODEL_ID }} | R3 | default | 1-2 min |
| 3 | Edge-case Reviewer | {{ MODEL_ID }} | R2 | off | 30-60s |
| 4 | Synthesizer | {{ MODEL_ID }} | R4 | extended | 2-4 min |
### Execution plan
- Round 1: Spawn roles 1-3 in parallel, then role 4 synthesizes
- Round 2: Roles 1-3 rebut, role 4 produces final synthesis
### Risk notes
- <token budget concerns>
- <any roles that may need fallback models>
Time estimation formula:
- Per role: look up "Est. time per role" from the profile in MODEL_TIERS.md
- Parallel roles in the same round: use the slowest role's time
- Sequential steps (synthesis after parallel): add times
- Multiply by number of rounds
- Add 1-2 minutes for orchestration overhead
The state file must follow this schema:
{
"run_id": "string — unique run identifier",
"topic": "string — the discussion/review/research topic",
"mode": "discussion | review | research",
"profile": "premium | balanced | budget | math-heavy",
"interaction": "star | debate | panel_judge",
"roles": ["string — role names in order"],
"models": {
"role_name": {
"model": "provider/model-id",
"thinking": "extended | default | off",
"reasoning_level": "R4 | R3 | R2 | R1"
}
},
"rounds_requested": 2,
"current_round": 0,
"status": "planning | running | paused | completed | failed",
"spawned_sessions": {
"role_name": "session-id or null"
},
"responses_received": {
"role_name": true
},
"pending_work": ["string — remaining tasks"],
"start_time": "ISO 8601 timestamp",
"estimated_duration_minutes": 10,
"recovery_needed": false,
"notes": ["string — post-hoc observations"]
}
After each round, write (use zero-padded numbering):
data/runs/<run_id>/round_01.mddata/runs/<run_id>/round_02.md
After synthesis, write:
data/runs/<run_id>/final.md
Spawning policy
The main agent is the orchestrator.
Prefer leaf subagents spawned directly by the main agent.
Subagent tool restrictions: spawned roles should only have access to tools they need for analysis and reasoning. They must NOT have access to:
gateway, cron — infrastructure managementsessions_spawn — no nested subagent spawninggroup:automation — no automated actionswrite, edit — only the orchestrator writes run state files
Subagents may use: read, web_search, web_fetch, group:memory (for context retrieval).
Use sessions_spawn for each participant contribution.
Each spawned task must include:
- the role
- the topic
- the role objective
- the expected response format
- the current round number
- only the minimum prior context needed
For opening statements, ask for:
- short position
- strongest argument
- one uncertainty or caveat
For later rounds, ask each role to:
- respond to the strongest counterpoint
- refine or defend its position
- provide one concession or one rebuttal
Recovery behavior
Subagent failure
Subagent announce-back can fail.
If a result is missing or the run was disrupted:
- Read
state.json — check status, current_round, responses_received, and pending_work
- Check which
round_XX.md files exist to find the last completed round
- Identify missing roles by comparing
responses_received against roles
- Set
recovery_needed: true and status: "running" in state.json
- Re-spawn only the missing roles from the last incomplete round
- Never discard already completed rounds unless the user asks
- If a role fails 2 consecutive times, skip it and note the skip in
pending_work
Token exhaustion
If a subagent's response is cut short (truncated output, token limit reached):
- Save whatever was received to the round file with a
[TRUNCATED] marker
- Re-spawn the same role with compressed context (summarize all prior rounds into 1-2 paragraphs)
- If the model's context window is too small, fall back to a model with a larger context window from the same tier or one tier down
- Update
state.json with the model change and reason
Gateway restart / inactivity interruption
If the orchestrator session is interrupted (gateway restart, inactivity timeout, connection drop):
- All state is on disk in
data/runs/<run_id>/
- On resume, the orchestrator (or user) says: "resume run <run_id>" or "continue the discussion"
- The orchestrator reads
state.json and all existing round_XX.md files
- It determines the last completed round and which roles responded
- It re-spawns only the missing work from the incomplete round
- Completed rounds and their files are never re-run
To make this work, the orchestrator must:
- Write
state.json before spawning each batch of subagents (not after)
- Update
state.json immediately after each response is received
- Write each
round_XX.md as soon as all responses for that round are in
Pause and resume
The user can pause a run at any time by saying "pause" or "stop for now".
On pause:
- Set
status: "paused" in state.json
- Note the pause reason and timestamp in
notes
- Do not spawn any new subagents
- Wait for any in-flight subagents to complete and save their responses
- Tell the user what was completed and what remains
To resume:
- The user says "resume", "continue", or "resume run <run_id>"
- Read
state.json — verify status is "paused" or "failed"
- Set
status: "running" and recovery_needed: true
- Continue from the last consistent checkpoint
Research templates
The user can request a template by name, or the orchestrator auto-selects based on task signals. If auto-selecting, briefly state which template was chosen and why before proceeding. The user can override.
Template auto-selection
| Task signal | Recommended template |
|---|
| "verify my proof", "check this theorem", "stress-test", "find holes" | Lakatos Proof & Refutation |
| "attack this problem", "explore complexity", "is this hard or easy", "open problem" | Pólya Multi-Strategy |
| "review my draft", "pre-submission review", "check exposition", "camera-ready" | Knuth Manuscript Review |
| General math/TCS claim, algorithm analysis, combinatorial argument | Structured Research Team |
| Token sliding/jumping, reduction proof, gadget verification, reconfiguration, PSPACE reduction | Graph Reconfiguration Specialist |
| "formalize this lemma", "Lean proof", "fix this sorry", "formalization" | Lean Formalization Team |
If multiple templates match, prefer the more domain-specific one. If uncertain, ask: "I'd recommend the [template name] for this — shall I proceed, or would you prefer a different template?"
Template chaining
When a task spans multiple concerns, chain templates as sequential phases within a single run. Each phase uses one template, and the output of one phase feeds into the next.
Common chains:
| Task | Phase 1 | Phase 2 | Phase 3 |
|---|
| "Verify this reduction and review the draft" | Graph Reconfig Specialist (correctness) | Knuth Manuscript Review (exposition) | — |
| "Explore this problem, then formalize" | Pólya Multi-Strategy (exploration) | Structured Research Team (pin down the claim) | Lean Formalization (formalize) |
| "Check my proof, fix it, then prepare for submission" | Lakatos (find holes) | Graph Reconfig Specialist (repair) | Knuth Manuscript Review (polish) |
| "Verify a gadget family and formalize the key lemma" | Graph Reconfig Specialist (verify) | Lean Formalization (formalize surviving lemma) | — |
How chaining works:
- Run Phase 1 to completion. Produce the standard final ledger.
- Pass only the Accepted claims and strongest surviving proof skeleton to Phase 2 as input context. Drop rejected/unresolved items unless Phase 2 is specifically about resolving them.
- Each phase gets its own round files:
round_P1_01.md, round_P1_02.md, round_P2_01.md, etc.
- The final output combines all phase ledgers into one, with phase annotations.
The orchestrator auto-detects chaining opportunities from task signals (e.g., "verify and review" → two phases). State the planned chain before starting: "I'll run this in 2 phases: (1) Graph Reconfiguration Specialist to verify correctness, (2) Knuth Review for exposition. OK?"
The user can also request chaining explicitly: "run Lakatos then Knuth on this draft."
Mandatory plan (all templates)
Before any template begins, the orchestrator must produce the plan output (see "Plan output format" section above) showing:
- Which model is assigned to each role (with reasoning tier R1-R4 and thinking level)
- Estimated time per role and total run time
- Profile used (math-heavy / premium / balanced / budget)
- Round execution order (which roles run in parallel, which are sequential)
For chained templates, show the plan for all phases upfront so the user can see the total estimated time and model usage before committing.
Mandatory preamble (all research templates)
Before any template begins, the orchestrator must also produce a Step 0 restatement:
- Rewrite the target claim in exact mathematical terms
- List all assumptions explicitly
- Separate what is given, what is to be proved, and what is only conjectured
- Identify the notation and definitions in use
Show this to the user and confirm before spawning agents. This catches misunderstandings before wasting compute.
Stop rule (all research templates)
If a decisive counterexample or fatal gap is found during any round:
- Stop defending the broken claim immediately
- Switch to diagnosis: what exactly fails and why
- Determine the strongest defensible corrected claim
- Do NOT continue expanding a broken proof across further rounds
Default output format for research-mode templates
The final synthesis must contain these sections:
1. Accepted — for each: statement, status (valid/partially valid), evidence, dependence list
2. Rejected — for each: statement, status (invalid), decisive reason, smallest counterexample if available
3. Unresolved — for each: statement, status (unclear), exact gap, missing evidence needed
4. Strongest surviving proof skeleton — shortest outline that currently survives all objections
5. Verification status — what was checked (SageMath, SAT/SMT, manual), what passed, what failed, what remains unchecked
6. Single recommended next action — choose exactly one: formalize / brute-force test / search for counterexample / weaken statement / redesign proof / redesign reduction / isolate sublemma
Template: Lakatos Proof and Refutation
Based on: Lakatos, I. (1976). Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press.
When to use: Stress-testing a new theorem or proof draft. Finding edge cases before submission.
Mode: review
Profile: math-heavy
Interaction: debate
Roles (4):
| # | Role | Reasoning | Task |
|---|
| 1 | Prover | R4 | Present the proof, defend the argument, propose fixes when flaws are found |
| 2 | Counterexample Hunter | R4 | Systematically search for counterexamples, boundary cases, degenerate inputs (empty graph, K₁, disconnected graphs, directed vs undirected). Use SageMath for computational checks. |
| 3 | Monster-Barrer / Refiner | R3 | When a counterexample is found, determine whether to restrict the hypothesis or strengthen the proof. Propose refined theorem statements. |
| 4 | Formalist | R4 | Check logical structure: are all quantifiers explicit? Are assumptions tracked? Does the proof use all hypotheses? Flag steps relying on unstated assumptions. |
Rounds (3):
Round 1 prompt for each role:
- Prover: "Present the claim and proof sketch. Identify the key steps and what each depends on."
- Counterexample Hunter: "Read the claim. List the hypothesis space. Identify the most likely failure points. Generate candidate counterexamples for small cases (n ≤ 7). Use SageMath if available."
- Monster-Barrer: "Read the claim. What graph classes or parameter ranges are NOT covered by the hypothesis? Where is the boundary?"
- Formalist: "Read the proof. List every assumption used (explicit and implicit). Check quantifier order. Flag any step that is not justified."
Round 2: Each role responds to the others' findings. Prover defends or concedes. Counterexample Hunter narrows the search based on Formalist's identified weak points.
Round 3: Synthesis. Formalist produces final assessment: (a) is the claim correct as stated? (b) what is the strongest version that survives? (c) what remains open?
Template: Pólya Multi-Strategy Problem Solving
Based on: Pólya, G. (1945). How to Solve It. Princeton University Press. See also: Pólya, G. (1954). Mathematics and Plausible Reasoning, Vols. I–II. Princeton University Press.
When to use: Attacking an open problem or conjecture where the right approach is unclear. Exploring the complexity boundary (hard vs tractable).
Mode: research
Profile: premium
Interaction: star (orchestrator collects, cross-pollinates, then re-distributes)
Roles (3):
| # | Role | Reasoning | Task |
|---|
| 1 | Specializer | R3 | Attack the problem on restricted instances (trees, paths, bounded treewidth, planar, small n). Find the boundary between easy and hard. Use SageMath for computational experiments. |
| 2 | Generalizer | R4 | Look for connections to known results. Can a known technique (Courcelle's theorem, color-coding, iterative compression, sunflower lemma) be adapted? Is this a special case of a solved problem? |
| 3 | Reducer | R4 | Assume the problem is hard. Search for a reduction source (3-SAT, NCL, Token Sliding on known-hard classes). Sketch gadget constructions. Identify which features make the problem hard. |
Rounds (3):
Round 1 prompt for each role:
- Specializer: "Solve or characterize the problem for: paths, cycles, trees, bounded treewidth ≤ 3, bipartite graphs, and small n (≤ 6). Report which cases are easy and which resist your attempts. Use SageMath to enumerate if needed."
- Generalizer: "Survey known results for related problems. List at least 3 known techniques that might apply. For each, explain why it might work and what obstacle might prevent it."
- Reducer: "Identify the 3 most promising reduction sources. For the top candidate, sketch the high-level gadget idea: what does each component encode? What invariant is maintained?"
Round 2: Orchestrator shares all findings. Each role reads the others.
- Specializer: "Given the Reducer's hardness sketch, can you find a small counterexample to the reduction? Given the Generalizer's technique suggestions, do any of them solve your remaining open cases?"
- Generalizer: "Given the Specializer's easy/hard boundary, can you identify the structural property that separates them? Does this match any known dichotomy theorem?"
- Reducer: "Given the Specializer's computational data, does it support or contradict your hardness conjecture? Refine your reduction sketch."
Round 3: Synthesis. Which strategy is most promising? What concrete next steps should the researcher take? Produce a ranked list of approaches with estimated difficulty and expected outcome.
Template: Knuth Structured Manuscript Review
Based on: Knuth, D.E., Larrabee, T., & Roberts, P.M. (1989). Mathematical Writing. MAA Notes No. 14. Mathematical Association of America. See also: Krantz, S.G. (1997). A Primer of Mathematical Writing. American Mathematical Society.
When to use: Reviewing a paper draft before submission. Preparing camera-ready version. Responding to referee reports.
Mode: review
Profile: premium
Interaction: panel_judge (three independent reviews, then judge synthesizes)
Roles (3):
| # | Role | Reasoning | Task |
|---|
| 1 | Correctness Reviewer | R4 | Read every proof line by line. Check: does each step follow? Are all cases covered? Are quantifiers correct? Are there unstated assumptions? Use SageMath to verify computational claims. Produce issues with severity: critical / minor / cosmetic. |
| 2 | Exposition Reviewer | R3 | Read as a non-specialist in the exact subfield. Check: is notation introduced before use? Are definitions self-contained? Is the paper readable top-to-bottom? Are examples helpful? Does the introduction motivate the work? Flag unclear passages. |
| 3 | Literature Reviewer | R3 | Check positioning: are all relevant prior results cited? Is comparison to related work accurate and fair? Are there missing connections? Are claimed novelties actually novel? Verify citations exist (no fabrication). |
Rounds (2):
Round 1 prompt for each role:
- Correctness: "Review the manuscript for mathematical correctness. For each issue, state: section, claim/proof affected, severity (critical/minor/cosmetic), and a specific fix suggestion. If a claim can be verified computationally, do so."
- Exposition: "Review the manuscript for clarity and readability. For each issue, state: section, the problem (unclear definition, notation clash, missing motivation, etc.), and a concrete rewrite suggestion. Follow Knuth's principle: a mathematical text should be readable as a story."
- Literature: "Review the manuscript's positioning. For each issue, state: the claim about novelty or relation to prior work, whether it is accurate, and what correction is needed. List any missing references that should be cited."
Round 2: Orchestrator collects all three reviews. Synthesizer (orchestrator itself) reconciles overlapping issues, removes duplicates, and produces a single prioritized action list:
- Critical correctness issues (must fix)
- Significant exposition problems (should fix)
- Missing/wrong citations (should fix)
- Minor issues (nice to fix)
- Cosmetic suggestions (optional)
Output integrates with instruction.md §28 (review validation) and STATE.md workflow.
Template: Structured Research Team
Adapted from a protocol designed for rigorous mathematical/TCS claim verification with independent roles and structured outputs.
When to use: Verifying a specific claim, proof, reduction, or structural characterization. The most rigorous template — use when correctness is paramount (e.g., before submitting a paper, or when a proof has already been questioned).
Mode: research
Profile: math-heavy
Interaction: star (independent first pass, then cross-critique)
Roles (4):
| # | Role | Reasoning | Task |
|---|
| 1 | Builder | R4 | Propose the strongest plausible proof strategy, algorithm, reduction, or structural characterization |
| 2 | Breaker | R4 | Search aggressively for hidden assumptions, quantifier mistakes, edge cases, counterexamples, broken gadgets, invalid inductions, missing directions, boundary failures |
| 3 | Alternative Builder | R4 | Produce a genuinely different route — not a paraphrase of the Builder. Must explain why the route is different and what advantage it offers. |
| 4 | Referee / Verifier | R4 | Synthesize only what survives scrutiny and external checking. Produce the final ledger. |
Rounds (3, with conditional round 4):
Round 1 — independent first pass. Builder, Breaker, and Alternative Builder work independently. Do not share results between them.
Builder must output:
- A. Precise claim version being attempted
- B. Strategy outline
- C. Intermediate lemmas needed
- D. Most fragile step (the step most likely to be wrong)
- E. Suggested external checks (SageMath computation, SAT encoding, brute-force, etc.)
Breaker must output:
- A. Strongest objection
- B. Exact failing step or most suspicious step
- C. Candidate counterexample or obstruction
- D. Whether the issue is fatal or plausibly repairable
- E. Minimal fix, if any
Alternative Builder must output:
- A. Alternative route
- B. Why it is genuinely different from the Builder's approach
- C. Key bottleneck
- D. Expected advantage over the Builder's route
- E. Likely failure mode of this alternative
Round 2 — one critique round. Each role critiques only decisive issues in the others' proposals.
- Focus on correctness, not style.
- If a decisive counterexample was found in Round 1, the Builder must not defend the broken claim — instead, propose the strongest defensible corrected version.
- Alternative Builder evaluates whether their route avoids the Breaker's objection.
Round 3 — external verification (run by orchestrator). Whenever feasible, run one or more of:
- Brute-force verification on smallest nontrivial instances (via SageMath)
- Python/Sage search for counterexamples to the claimed statement
- Explicit dependency audit (does each step actually use only what it claims?)
- SAT/SMT/ILP encoding for finite verification
- Citation/reference check for any imported fact (mark unverified as [unchecked])
Round 4 — optional repair round. Run ONLY if:
- There is a concrete local repair (not a fundamental redesign)
- The Breaker confirms the repair addresses the specific failure
If the issue is structural, skip Round 4 and recommend "weaken statement" or "redesign proof" in the final ledger.
Final output: Uses the mandatory research output format (Accepted / Rejected / Unresolved / Proof skeleton / Verification status / Single next action).
Hard rules for all roles:
- Correctness over elegance
- Distinguish explicitly: proved / heuristic / conjectural / unverified
- Never suppress dependence on an unproved subclaim
- Check both directions of every iff/equivalence
- Check boundary cases explicitly (n=0,1,2,3; empty graph; disconnected; directed vs undirected)
- Do not use "WLOG" unless justified
- Do not smooth over nonlocal interactions in reductions or gadget arguments
- Prefer a weaker correct theorem over a stronger broken one
- If using literature facts, mark any unverified citation as [unchecked]
- If no external verification is possible, say so explicitly
Template: Graph Reconfiguration Specialist
Domain-specific variant of the Structured Research Team, tailored for token sliding/jumping, reduction proofs, gadget verification, and reconfiguration complexity.
Informed by: Wang et al. (2024). "Rethinking the Bounds of LLM Reasoning: Are Multi-Agent Discussions the Key?" ACL 2024. (Sparse communication with independent roles outperforms long all-to-all debate.) Huang et al. (2024). "Large Language Models Cannot Self-Correct Reasoning Yet." ICLR 2024. (External verification is crucial; intrinsic self-correction is unreliable.)
When to use: Proving PSPACE/NP-hardness or polynomial solvability for a reconfiguration problem. Repairing a broken reduction. Verifying a gadget family. Checking a theorem in a draft. Analyzing a reconfiguration algorithm. Preparing a claim for formalization.
Mode: research
Profile: math-heavy
Interaction: star (sparse: independent work, then compressed cross-critique)
Roles (4):
| # | Role | Reasoning | Task |
|---|
| 1 | Constructor | R4 | Propose the strongest plausible proof strategy, reduction, algorithm, or repaired statement |
| 2 | Adversary | R4 | Search aggressively for counterexamples, hidden assumptions, broken iff directions, missing cases, unintended moves, nonlocal interference, boundary failures |
| 3 | Auditor | R4 | Perform structured auditing in two separate layers: (A) local/interface audit, (B) global/correspondence audit |
| 4 | Referee / Verifier | R4 | Maintain the claim ledger. Downgrade claims immediately when verification fails. Accept only what survives objections and explicit checks. |
Claim ledger (initialized in Step 1, updated throughout):
For every candidate claim, track:
- ID, statement
- Status: proved / refuted / unclear / heuristic
- Confidence: high / medium / low
- Dependencies (list of claim IDs this depends on)
- Verification type: formal / exhaustive / symbolic / computational / bibliographic / none
- Owner (which role is responsible)
- Notes
Rounds (3, with conditional round 4):
Round 1 — independent first pass. Constructor, Adversary, and Auditor work independently.
Constructor outputs:
- A. Exact claim version attempted
- B. Proof/reduction/algorithm outline
- C. Required intermediate lemmas
- D. Most fragile step
- E. Suggested external checks
- F. Whether the claim may need weakening
Adversary outputs:
- A. Strongest objection
- B. Exact failing step or suspicious step
- C. Candidate counterexample / obstruction
- D. Fatal or repairable?
- E. Smallest plausible fix
Auditor outputs TWO SEPARATE sections:
A. Local/interface audit:
- Gadget ports / attachment vertices are unambiguous
- Legal moves inside the gadget are exactly characterized
- Token count / occupancy / independence / orientation legality preserved
- No hidden assumptions on adjacency, reachability, or exclusivity
- Planarity / permutation / interval / graph-class constraints locally respected
- Completeness and soundness at the gadget level are both addressed
B. Global/correspondence audit:
- Gadgets do not create unintended cross-gadget moves
- Local simulations compose correctly
- Source states correspond to target states
- Legal reconfiguration sequences map in both directions if claimed
- No global invariant is silently violated
- No serialization / normalization claim is used without proof
- Target instance size is polynomial and construction is well-defined
- Both directions of any equivalence are justified separately
Round 2 — one critique round. Adversary and Auditor critique Constructor. Constructor may respond only to decisive issues. No long debate. If a decisive counterexample exists, stop defending and switch to diagnosis.
Round 3 — external verification (run by orchestrator via SageMath). Run these checks explicitly and separately:
A. Computational — brute force smallest instances, enumerate states/moves, search for unintended moves, test claimed invariants
B. Structural — graph-class membership, planarity/embedding constraints, orientation legality, degree/interface constraints, polynomial-size sanity check
C. Bibliographic — verify imported theorems actually state what is claimed, mark [unchecked] otherwise
D. Formal — if formalization is attempted, the checker is final authority
Round 4 — optional repair. Run ONLY if there is a concrete local repair. Otherwise choose one: weaken statement / isolate missing lemma / redesign gadget / redesign correspondence / abandon equivalence and keep one direction / replace global claim by conditional.
Typed verifier table (in final output):
| Check type | Target | Passed/Failed/Not run | Limitations |
|---|
| Computational | gadget X on n≤6 | passed | n≤6 only |
| Structural | planarity of construction | passed | — |
| Bibliographic | [Author, Thm 3.1] | [unchecked] | no access to full text |
| Formal | Lean skeleton | not run | — |
Failure taxonomy for reductions (use in rejection reasons):
- Local gadget unsoundness (admits an illegal configuration)
- Local gadget incompleteness (blocks a legal configuration)
- Cross-gadget interference (unintended moves between gadgets)
- Illegal move admitted (reduction allows a move that shouldn't exist)
- Legal move missing (reduction blocks a move that should exist)
- State correspondence broken (source/target states don't match)
- Equivalence overstated (only one direction holds)
- Graph-class preservation broken (construction leaves the target class)
- Planarity/orientation broken
- Polynomial-size claim broken
- Imported lemma/citation unsupported
Hard rules (in addition to global hard rules):
Every reduction proof must separate: (i) construction, (ii) local gadget behavior, (iii) completeness, (iv) soundness, (v) noninterference, (vi) size/class preservation.
Every algorithmic proof must separate: (i) move legality, (ii) progress measure / termination, (iii) completeness, (iv) soundness, (v) runtime.
Never merge prose polishing with proof repair. Stabilize correctness first.
Final output: Uses the mandatory research output format (Accepted/Rejected/Unresolved + proof skeleton + typed verifier table + single next action). Add "Draft-repair notes" section if the task concerns a manuscript.
Template: Lean Formalization Team
For formalizing a single graph-reconfiguration lemma in Lean 4. Not for proof discovery — use one of the other templates first, then formalize what survives.
When to use: Formalizing a specific lemma that has already been proved on paper. Debugging a stuck Lean proof. Decomposing a large formal goal into manageable pieces.
Mode: research
Profile: math-heavy
Interaction: star
Roles (5):
| # | Role | Reasoning | Task |
|---|
| 1 | Informal Planner | R4 | Decompose the lemma into minimal subclaims. Map each subclaim to the proof strategy. |
| 2 | Formalizer | R4 | Write a conservative compiling Lean scaffold. Preserve compiling state at every step. |
| 3 | Missing-Lemma Miner | R3 | List the smallest auxiliary lemmas needed. Check Mathlib for existing versions. |
| 4 | Repair Agent | R3 | Classify each blocker: syntax / type / coercion / missing lemma / wrong induction / statement too strong / impossible goal |
| 5 | Checker | R4 | Final authority. Decide: complete / locally fixable / blocked on helper lemma / blocked on statement / blocked on missing idea |
Rounds (2):
Round 1:
- Informal Planner produces subclaim decomposition
- Formalizer writes initial scaffold with
sorry placeholders
- Missing-Lemma Miner searches Mathlib and lists available/missing lemmas
Round 2:
- Repair Agent classifies each
sorry and proposes fixes
- Checker evaluates: which sorries are closable, which need new helper lemmas, which indicate the paper proof has a gap
Hard rules:
- One lemma at a time
- Preserve compiling state whenever possible
- Distinguish mathematical gap from formalization gap (a proof can be correct but hard to formalize, or incorrect but easy to formalize)
- Do not claim completion unless the Checker accepts
Final output:
- Lean file with status of each sorry (closable / needs helper / blocked)
- List of missing Mathlib lemmas
- Assessment: is the paper proof correct as stated, or does formalization reveal a gap?
Final output
Return a polished result with these sections:
- Topic
- Mode
- Roles used
- Models assigned
- Interaction pattern
- Rounds completed
- Main agreements
- Main disagreements
- Best points by role
- Final synthesis
- Recommended next step
Also include a compact run summary:
- run id
- profile used
- number of agents and their models
- thinking levels used
- rounds completed
- actual duration vs estimated duration
- whether recovery or pause/resume was needed
- whether any responses were truncated or models were swapped
