/propose-subgoal-decomposition-plans

name: propose-subgoal-decomposition-plans
description: Propose multiple subgoal decomposition plans for the current theorem using the information already gathered. Use when enough information has been collected from examples, counterexamples, search results, and previous failures to break the problem into several materially different plans.

Propose Subgoal Decomposition Plans

Use this skill when the agent has enough context to propose several viable decomposition plans.

Input Contract

Read:

• the current target theorem or branch goal
• relevant `immediate_conclusions`, `toy_examples`, and `counterexamples`
• relevant `failed_paths` and `branch_states`
• recent search results and useful references from `events`

Procedure

1. Gather the current information that materially constrains the problem: useful examples, failed claims, known obstructions, and relevant search results. 2. Propose materially different decomposition plans. 3. For each plan, state:

• the main idea of the plan
• the ordered subgoals
• why this plan is plausible given the current information
• which earlier failures or counterexamples it tries to avoid

4. Hand each plan to `$direct-proving` for a quick screening pass.

Output Contract

Publish one plan per decomposition to global memory with `gm_add` (kind `plan`, a judgment — `verifiable=false`): `claim` = the plan's goal + summary, `evidence` = its motivation, plus these fields:

{
  "plan_id": "...",
  "record_type": "decomposition_plan",
  "goal": "...",
  "plan_summary": "...",
  "subgoals": ["..."],
  "motivation": ["..."],
  "uses_information_from": {
    "examples": ["..."],
    "counterexamples": ["..."],
    "key_failures": ["..."],
    "search_results": ["..."]
  },
  "status": "proposed|screening|screened|selected|failed|solved",
  "branch_id": "optional"
}

Also note the new plan set in your local memory (`events`).

Tools

• `gm_add` (publish the plan findings)
• `gm_search` (recall the examples/counterexamples/dead-ends the plans build on)
• `search_arxiv_theorems`

Failure Logging

If the agent cannot yet propose meaningful decomposition plans, append an `events` record with:

• `event_type="decomposition_plans_not_ready"`
• the missing information
• the blockers that prevent proposing plans