Brainstorm

各手法は以下の形式で記述する:

## 手法 N: [タイトル]
- **カテゴリ**: [上記10カテゴリの1つ]
- **概要**: [1-2文で何をやるか]
- **期待される成果**: [何が分かりそうか]
- **必要なツール**: python / lean / websearch / analysis
- **推定難度**: 低/中/高
- **新規性**: [過去の探索と何が違うか]
- **形式化ポテンシャル**: [Lean形式化の可能性 — なし/補題候補/定理候補/副産物候補]

形式化ポテンシャルが高い手法は、たとえ主予想への直接的インパクトが小さくても優先度を上げる。 sorry なしで証明できる定理は、それ自体が成果になる。

A3. 優先順位付け

生成した手法を以下の基準で順位付けする:

• 成功確率: 何か新しい発見が得られそうか
• 影響度: 発見できた場合のインパクト
• 形式化価値: Lean証明として残せるか（副産物としての独立した価値があるか）
• 過去の探索との差異: 既にやったことの焼き直しでないか
• 実行可能性: subagent 1体が10-15分で完了できるか

A4. queue.json への書き込み

全手法を Unsolved/explorations/queue.json に追加する。

各エントリの形式:

{
  "id": "[problem]-NNN",
  "problem": "[problem]",
  "title": "手法のタイトル",
  "category": "カテゴリ名",
  "description": "詳細な説明（subagentへの指示として十分な量）",
  "expected_output": "期待される成果",
  "tools": ["python"],
  "priority": 1,
  "status": "queued",
  "formalization_potential": "なし / 補題候補 / 定理候補 / 副産物候補",
  "created": "YYYY-MM-DD"
}

status は queued | in_progress | done | skipped のいずれか。

フェーズB: subagent並列調査ディスパッチ

B1. subagent の起動

queue.json から status: "queued" のアイテムを最大 5件ずつ 選び、 1つのメッセージで5体のsubagentを同時にAgent ツールで起動する。 全20件を消化するまで B1→B2 を 4ラウンド 繰り返す。

各subagentへのプロンプトは /explore-batch と同じ形式を使用する。 ただし以下の情報をコンテキストに含めること:

• 問題概要（problems.md から）
• 既知の重要事実（SUMMARY.md + INDEX.md から5-10項目）
• 形式証明済み主要定理（Index.lean から5項目）
• Leanプロジェクト構造マップ

subagent設定:

• subagent_type: "math-explorer" — 専用の探索エージェントプロファイルを使用
• model: "opus" — 全subagentでOpusを使用
• description: 手法タイトルの先頭3-5語
• Lean形式化を含む場合: isolation: "worktree"
• run_in_background: true — バックグラウンドで並列実行

B2. 結果の収集・記録

全subagentの結果が返ったら:

1. 各結果を Unsolved/explorations/[problem]/exploration_NNN.md に保存
2. INDEX.md に行を追加
3. queue.json の各アイテムを "done" に更新

B3. 残りのキュー処理

まだ queued が残っている場合、次の5件で再度 B1→B2 を実行する。 全20件を消化するまで繰り返す（計4ラウンド）。

重要: 各ラウンドでは前ラウンドの全subagentの完了を待ってから結果を記録し、次の5件を起動する。

フェーズC: バッチ完了報告

全subagentの結果を横断分析し、以下を出力:

## ブレインストーム結果
- 生成した手法: N件
- 調査完了: M件
- 成果: 大発見 x件, 中発見 x件, 小発見 x件, なし x件
- 形式化候補: x件

## 主要な発見
1. [最も重要な発見]
2. [次に重要な発見]

## 形式化候補（Lean証明として残す価値があるもの）
- [候補1 — 関連モジュール: Collatz.XXX]
- [候補2]

## 有望な仮説
- [仮説1]

## 次のアクション
- `/explore-aggregate [problem]` で集約推奨

重要な原則

• 広く浅く: 手法生成フェーズでは深掘りしない。アイデアの量を重視
• 過去の失敗を活かす: SUMMARY.mdの「行き止まり」は二度やらない
• 視点の多様性: 同じカテゴリに偏らない
• 実行可能な粒度: 「コラッツを解く」ではなく「mod 16での下降率を計算する」
• 形式化意識: 副産物でもよいので、形式証明として残せる成果を意識する
• subagentにファイル編集させない: Lean/主要ファイルの編集はメインエージェントが集約後に行う
• 並列起動必須: subagentは逐次ではなく並列で起動する