mcpField
S
siege

siege

github.com/anthropicsその他45.1k798 回インストール1 日前に更新
リポジトリ

siege について

siegeは、math-proofの多ラウンド型証明オーケストレーションスキルです。数学の問題を複数のワーカーエージェントに分け、ジャッジエージェントが確認し、主張と目標を管理しながら、状態を明記したproof.mdを作成します。

主な機能

  1. 01問題を独立したクエリに分割
  2. 02ジャッジエージェントによる推論確認
  3. 03主張を台帳で管理
  4. 04ラウンドと高負荷の作業波に対応
  5. 05最終proof.mdの作成と確認

活用シーン

  1. 01複雑な証明の並行的な推進
  2. 02証明済み・反証済み・未解決の主張の追跡
  3. 03複数ラウンドにわたる完全な証明の確認

インストール

コマンドをコピーしてターミナルで実行します。

$npx skills add https://github.com/anthropics/claude-plugins-official --skill siege

インストール後、Claude Code で/siegeを入力して読み込まれたか確認します。

同梱ファイルscripts/ledger.py

詳細

math-proof: siege

アプローチ

このスキルでは、1つの問題に最大 MAX_ROUNDS ラウンド取り組みます。各ラウンドで、審判は自己完結した質問をいくつか作成します。ラウンド ESC_ROUND までは、質問数は最大 WAVE です。以下の手順では、これらをクエリと呼びます。各質問は、新たに起動され、その質問と問題文だけを参照できるワーカーに送られます。審判は回答を読み、進行中の要約を書き直し、PROVED、REFUTED、OPEN のいずれかの印を付けた主張を台帳に追加します。主張の1つは目標で、ラウンド1に設定します。審判は後のラウンドで新しい目標を設定してもかまいません。特に、目標が証明されたら、より重要な主張へ引き上げてもかまいません(証明済みの目標はその後もフォールバック結果として台帳に残ります。2回のウェーブを経ても引き上げた目標に近づかなければ、審判はその結果に戻ります。目標を引き上げたときは、ユーザーに伝え、証明済みの結果を DIR/result-so-far.md にコピーします)。回答に目標の完全な証明または反証が記されている場合、さらに2人のワーカーがその正確なテキストを行ごとに確認します。両者が合格と判断したら、審判は結論を出すか、目標を引き上げます。ラウンド MIN_ROUNDS より前に結論を出すには、この方法だけが認められます。ラウンド ESC_ROUND 以降、完全な証明または反証が得られていない場合は、より多くの労力をかけるワーカー向けに、1ラウンドで最大 WAVE_DEEP 個の質問を用意できます。そのうち最大2つを除くすべては、証明に残されている唯一の主張を目指します。ラウンド終了後、審判が自己完結した proof.md を書き、ワーカーが確認してから、審判が最終版に仕上げます。実行終了時の目標がラウンド中に証明され、2回の確認も済んでいない場合は、最終版に仕上げる前に追加の修正パスと、完全な証明を試みる最後のウェーブも行います。proof.md には、何が証明され、何が証明されていないかを明確に記した Status セクションがあります。このセクションは要約にすぎません。あなた自身は数学を一切行わず、以下の手順に厳密に従って、審判の各ステップと各ワーカーのために新しいサブエージェントを起動します。

あなたはこのプロトコルのオーケストレーターです。あなた自身は数学を行わず、判断もしません。判断は、ステップごとに新しい math-proof-judge サブエージェントが行い、推論は、クエリごとに新しい math-proof-worker または math-proof-worker-deep サブエージェントが行います。どちらを使うかはラウンド番号によって決まります(「ルール」を参照)。あなたの役割は、以下の手順を厳密に実行し、ファイルを整理し、記録スクリプトが出力する唯一の機械的な判定に基づいて行動し、問題が簡単または難しそうに見えるという理由で手順を省略、統合、並べ替えないことです。ワーカーの回答ファイルは自分で読まないでください(存在するかどうかは test -s で確認してください。完了したかどうかを判断するのはあなたではなく、記録スクリプトです)。審判が読む場所では、数学の内容を自分の言葉で要約しないでください。言い換えではなく、ファイルを渡してください。最後まで無人で作業を続けてください。質問に答える人はいません。 引数。 呼び出しメッセージには、次のように記述されています:$ARGUMENTS 問題と、任意で設定が指定されています。次のように読み取ってください。先頭にある NAME=value 形式のトークンは、NAME が2文字以上の大文字とアンダースコアからなる語で、value が整数の場合(DIR の場合はパスで、空白を含むときは引用符で囲まれています)、設定です(以下の7つ、または実行ディレクトリを表す DIR)。それ以外の NAME はエラーです(「Settings」を参照)。これらを削除してください。残った部分全体が、前後の空白と一組の囲み引用符を取り除き、バックスラッシュでエスケープされた空白を空白として解釈したとき、既存ファイルのパスとなる1行だけであれば、そのファイルが問題ファイルです(空白を含んでもかまいません。シェルではなく Read または Glob で確認してください)。該当するファイルが存在せず、残った部分がファイルパスとしか解釈できない場合(.md、.txt、.tex で終わる1行、または引用符を除くと空白を含まず、"/" または "" を含む1つのトークン)は、探した絶対パス(そのパスを示してください)にファイルが存在しないこと、代わりにコマンドの後ろに問題文全体をテキストとして指定できることを、1文でユーザーに伝えて終了してください。それ以外の場合、残った部分はメッセージの末尾まで、数学、改行なども含め、そのまま問題文です(MAX_ROUNDS=8 は設定ですが、「n=3」、「N=pq」、「AB=AC」、「f(x)=…」は数学です)。実行ディレクトリ DIR の既定値は、現在のディレクトリ以下の ./math-proof-run です。以降はすべて DIR の絶対パスを使用してください。メッセージに読み取り可能な問題ファイルも問題文も含まれていない場合は、/math-proof:siege [NAME=value …] <problem statement, or the path of a file holding it> という使用方法と、停止した実行は同じディレクトリで元の行を再度指定すれば再開されることを、1~2文で伝えて終了してください。

設定(呼び出しメッセージで指定されない限り、以下を使用してください):ESC_ROUND = 4(エスカレーションラウンド。ESC_ROUND 以降のラウンドもループが続いている場合、ウェーブ上限が引き上げられ、すべてのワーカーが math-proof-worker-deep になり、計画概要にエスカレーション条項が含まれます);WAVE = ESC_ROUND より前のラウンドで、1ラウンドあたり最大4件のクエリ。WAVE_DEEP = ESC_ROUND 以降のラウンドで、1ラウンドあたり最大10件のクエリ;MAX_ROUNDS = 14;MIN_ROUNDS = 4(MIN_ROUNDS 以降はジャッジが自由に結論を出せます。それ以前は、台帳に監査済みの連鎖がある場合に限ります。判断はスクリプトが行います);REFINE_STEPS = 2;MAX_COMMIT = 9(どちらも完全な証明の後段に適用されます。ラウンド中に最終目標が証明済みと判定された実行では、短い後段になります。「The proof tail」を参照してください)。呼び出しメッセージの先頭、問題文の前に NAME=value 形式のトークン(たとえば MAX_ROUNDS=8 WAVE_DEEP=6)を置くことで、7つの設定のいずれも名前で上書きできます。指定された値を使用してください。そこで NAME が7つの設定にも DIR にも該当しないトークン(NAME が2文字以上の大文字とアンダースコアからなる語で、value が整数の場合)があればエラーです。その場合、NAME は /math-proof:siege の設定ではないこと、受け付ける名前は DIR、ESC_ROUND、WAVE、WAVE_DEEP、MAX_ROUNDS、MIN_ROUNDS、REFINE_STEPS、MAX_COMMIT であること、そのトークンが問題の一部ならファイルパスで問題を指定できることを、1文でユーザーに伝えてください。何も作成する前に終了してください。(左辺が1文字だけ、またはすべて大文字ではない先頭トークン、右辺が整数ではないトークン、および問題文のさらに後にある「=」は、設定ではなく数学です。) 以下で設定名が使われている場合は、その時点で有効な値を指します。 記録管理スクリプトは、このスキル自身のフォルダーにある scripts/ledger.py です:python3 ${CLAUDE_SKILL_DIR}/scripts/ledger.py(以下、SCRIPT と呼びます)。そのプレースホルダーが置換されておらず、/scripts より前のパスが存在しない場合は、${CLAUDE_PLUGIN_ROOT}/skills/siege/scripts/ledger.py を使用してください。こちらも置換されていない場合は、~/.claude 以下で **/skills/siege/scripts/ledger.py を Glob し、絶対パスを使用してください(複数見つかった場合は最新のものを使用します)。いずれの場合も、スクリプトのパスに空白が含まれるときは、コマンド内で引用符で囲んでください。Setup の前に、追加の引数なしで SCRIPT を1回実行してください。「usage:」で始まる行が出力されるはずです。代わりに Python が実行されてもスクリプトファイルを開けないと表示される場合、Python ではなくパスが間違っています。上記の代替手段で再度解決してから、もう一度実行してください。ledger.py が見つからない場合は、プラグインのファイルが想定された場所にないこと(/plugin から math-proof を再インストールしてください)をユーザーに伝えて終了してください。代わりにシェルから python3 が見つからないと言われる場合、または usage 行以外の応答が返ってきた場合(Windows で、Python を「見つけられませんでした」と表示され、Store からインストールできるという応答もこれに該当します)は、以降 SCRIPT では python3 の代わりに python を使用し、もう一度実行してください。それも失敗した場合は、/math-proof:siege が記録管理スクリプトを実行できなかったこと、コマンドとシェルの応答を引用すること、PATH 上で python3 または python として Python 3.7 以降が必要であること、問題が解決したら同じ行を再度指定すれば実行できることを、1~2文でユーザーに伝えて終了してください。

セットアップ

  1. DIR/state.md がすでに存在する場合、これは再開です。既存の DIR/problem.md が渡されたものと同じ問題かどうかを確認してください(空白と改行コードの違いは無視してテキストを比較します。ファイルの場合は cmp を使用します)。異なる場合は、DIR には別の問題に対する実行結果が保存されていること、および DIR=<another directory> で新しい実行先を選択できることを一文で伝えて、停止します。同じ問題で、state.md に「phase: finished」と記録されている場合、その実行は完了しています。DIR/proof.md の場所(存在する場合は DIR/result-so-far.md も)、および DIR=<another directory> で新しい実行を開始できることを伝えて、停止します。それ以外の場合は、DIR/problem.md を全文読み、state.md を読んで、最初から開始せず、記録されているフェーズから再開します。出力ファイルが存在するステップは再実行せず、DIR/problem.md も書き換えないでください(呼び出しメッセージで指定された設定が state.md に記録された設定と異なる場合は、次のツール呼び出しと同じメッセージに、記録された設定がこの実行を規定することを一行で記載します。これは通知であり、停止の指示ではありません)。記録されたフェーズが wave の場合、その wave のクエリの語幹について SCRIPT answers を実行し(Rules の wave ルールを参照)、スクリプトが回答済みと報告しなかったクエリに対してのみワーカーを起動します。部分的なものにはそれぞれ {EARLIER} 段落を付けます。この起動を wave の最初の実行として数えるため、1 回の再実行も通常どおり行います。すでに回答済みでインデックス行がないクエリには、"{Q} | answered | (finished before this session resumed)" という行を追加します。すでにインデックス行があるクエリには行を追加せず、その行に「 | re-run: status | abstract」として新しいステータスを追記します。それ以外の場合は、DIR と DIR/judge/ を作成し(mkdir -p)、問題を DIR/problem.md に保存します。問題がファイルとして渡された場合は、そのファイルを cp でバイト単位でそのままコピーします。呼び出しメッセージ内のテキストとして渡された場合は、そのテキストだけを一切追加・削除・言い換えずに DIR/problem.md に書き込みます。その後、次のアクションとして DIR/problem.md を全文読みます。テキストはすべての判定者向け概要とワーカープロンプトに貼り付けます(Rules を参照)。
  2. DIR/state.md に、protocol math-proof siege、適用する値を伴う7つの設定(呼び出しメッセージによって上書きされたものには印を付けます)、および「phase: round 1 plan, attempt 1」を記載します。再開時は state.md に記録された値を適用します。

ラウンドループ — r = 1, 2, …, MAX_ROUNDS の各ラウンド

(a) 計画。 math-proof-judge を1つ起動します。そのプロンプトには、下記の PLAN BRIEF に {r}、DIR、ラウンドに応じたスロットを埋めたものを使います(再試行時は、スクリプトから与えられた修正段落を先頭に追加します)。スロットは次のとおりです。 {CAP} はこのラウンドのクエリ数の上限です。r < ESC_ROUND のときは Setting WAVE、r ≥ ESC_ROUND のときは Setting WAVE_DEEP の値を使います。また、(b) のチェックコマンドにも同じ数値を指定します。{MAX_ROUNDS} は MAX_ROUNDS の設定値を数値で記入します。{HORIZON}、{CONCLUDE_RULE}、{ESC_SUMMARY}、{ESC_WAVE} には、この r のブリーフの後に示されているテキストを入れます(ESC_ROUND より前のラウンドでは空のスロットが複数あります。空のスロットには、スペースや空行も含め何も挿入しません)。これはラウンド r の試行 1 です。 (b) チェック。 まず、DIR/judge/screen_r{r-1}.md が存在し、DIR/index.md のラウンド r−1 の行にまだスクリーニング判定が記載されていない場合、その判定(" | OK" または " | DEGENERATE: …")を各クエリのインデックス行に追記します。これは通常のファイル操作です。DEGENERATE 判定があっても再実行はしません。次に SCRIPT check DIR {r} {CAP} {MIN_ROUNDS} {attempt} を実行します({CAP} はこのラウンドの上限値 WAVE または WAVE_DEEP で、(a) と同じ値です。ラウンド ESC_ROUND 以降で WAVE を渡すと、波の一部が黙って除外されます)。スクリプトはラウンドの台帳行を採番して DIR/ledger.md に追記し、判定行を1行だけ出力します。その最初の語に従って処理します(代わりに ERROR: で始まる行が出力された場合、コマンド自体の形式が誤っています。まず DIR を絶対パスで指定し、その後に4つの数値を指定します。コマンドを修正して再実行してください。これは計画の試行回数には含まれません)。

  • WAVE n FLOOR f … — DIR/round{r}_summary.md を DIR/summary.md にコピーし、f を記録します(この波で回答済みまたは部分回答として返されるクエリの最小数です。Rules を参照)。目標変更の通知が必要なら下記の通知を行い、クエリファイル DIR/round{r}_q1.md … DIR/round{r}_q{n}.md を使って (c) に進みます(必要に応じてスクリプトが番号を連続したものに振り直しています)。
  • CONCLUDE … — DIR/round{r}_summary.md を DIR/summary.md にコピーし、この判定行をループ終了の理由として state.md に記録します。目標変更の通知が必要なら下記の通知を行い、ループを抜けて証明の後処理に進みます。
  • RETRY: <correction> — 計画ステップ (a) を次の試行として再起動し、"RETRY: " の後のテキストをブリーフの先頭段落に追加します。その後、試行番号を1増やして (b) を再度実行します。
  • TAIL: <reason> — 計画ステップが3回失敗しました。理由を state.md に記録し、DIR/round{r}_summary.md が存在し空でなければ DIR/summary.md にコピーして、ループを抜けて証明の後処理に進みます。ただし、DIR/summary.md が存在せず、.answer.md または .partial.md ファイルも一切存在しない場合(下書きの材料がない場合)は、そこで停止して報告します。 目標変更の通知:WAVE または CONCLUDE 判定の場合、その判定を受け入れた計画起動の応答(最新の試行)に "Goal change:" で始まる文があれば(判定役がこのラウンドで目標を置き換えた、引き上げた、または元に戻した場合。ブリーフの項目 2)、その文を引用符で囲み、次のツール呼び出しと同じメッセージ内に1行のテキストとしてユーザーに伝えます(質問ではなく通知です。テキストだけのメッセージではターンが終了するため、停止したり応答を待ったりしないでください)。同じ行を state.md にも記録します。文が "Goal change: raised" で始まる場合は、以前の目標の証明が保持されているものとして文中で指定されたファイルを DIR/result-so-far.md にコピーします(それぞれに対して test -s を実行します)。ファイルが1つなら cp、複数なら cat <files in the order named> > DIR/result-so-far.md(それぞれに独自の終端行があるため、それが区切りになります)を使い、以前の result-so-far.md があれば上書きします。また、通知行の末尾に "the proved result so far is in DIR/result-so-far.md" を付けます。文でファイルが指定されていない場合は、DIR/ledger.md の "N. PROVED: [GOAL] …" 形式の最後の行にある最終 "—" の後のロケーターから を取得し(grep)、DIR/<stem>.answer.md を使います。そのファイルがない場合は DIR/<stem>.partial.md を使います。各ファイルに対して先に test -s を実行し、どちらも存在しなければコピーを省略し、その旨を通知行に記載します。このファイルはここで実行を止めるユーザー向けです。以降の処理では読み込まれず、実行の成果物は引き続き proof.md です。(主張が固定された問題では、目標の引き上げは起きません。引き上げ先がないため、ファイルは書き込まれません。ただし、置き換えは引き続き通知されます)。 いずれの場合も、実際に波が実行された最後のラウンド番号 R を state.md に記録します((c)~(d) の完了後は R = r、波を実行する前にラウンド r でループを抜けた場合は R = r−1、波が一度も実行されていない場合は R = 0)。DRAFT BRIEF でこの値が必要になります。 (c) 波。 ラウンドのクエリファイルで波を実行します(Rules を参照。各ファイルにつきワーカー1つ。ESC_ROUND より前のラウンドでは math-proof-worker、ラウンド ESC_ROUND 以降では math-proof-worker-deep を使います。すべて1つのメッセージで実行し、スクリプトの answers 判定、インデックス行、未回答クエリの再実行1回を行った後、FLOOR 停止ルールに従います)。 (d) スクリーニング(起動なし)。 独立したスクリーニングステップはありません。次のラウンドの計画判定役がこの波の回答を自らスクリーニングし(PLAN BRIEF、項目 0)、DIR/judge/screen_r{r}.md に書き込みます。次のラウンドの (b) で、その判定をインデックスにコピーします。state.md を更新し("phase: round {r+1} plan, attempt 1"、R = r)、ループを続けます。

証明の仕上げ(ループが終了した後、CONCLUDE、TAIL、またはラウンド MAX_ROUNDS の完了による)

まず、仕上げの形式を決めます。SCRIPT gate DIR を実行します。出力が CONCLUDE で始まる場合、claims ledger では主要目標が確定済みであり、2 回の個別の verify クエリによって証明済みです。仕上げは SHORT です。(e)draft、(f)refine ステップなし、select ステップなし — 下記(g)に記載のシェル連結で DIR/r3_verify.md を自分で作成し、r3_q ファイルは書き込みません —、(h)DIR/r3_verify.md のみを含む commit wave、(i)finalize。それ以外(通常は REJECT: …)が出力された場合、仕上げは FULL です。以下に記載のステップ(e)〜(i)をそのまま実行します。ただし、ERROR: で始まる行は gate コマンド自体の形式が誤っていることを意味します(DIR を最初に、絶対パスで指定)。判断する前に修正して再実行してください。state.md に「tail: short」または「tail: full」と、gate の行を記録します。SHORT の仕上げには 2 つのフォールバックがあります。verify のみの wave が 1 回の再実行後も DIR/r3_verify.answer.md なしで終わった場合、(g)から FULL の仕上げに切り替えます(「tail: short, then full — no verify answer」と記録)。また、SHORT の仕上げにおける最初の finalize の応答が「MAIN CLAIM: NOT PROVED」で始まる場合(ステップ(i)の単独 grep チェックより前に確認)、証明済みの連鎖が verify クエリで維持されなかったことになります。state.md に「tail: short, then full」と記録し、DIR/r3_verify.md および(存在する場合)DIR/r3_verify.answer.md をそれぞれ DIR/r3_verify.first.md/DIR/r3_verify.first.answer.md に名前変更します。同様に、DIR/r3_verify.partial.md があれば DIR/r3_verify.first.partial.md に名前変更します(r3_verify のインデックス行に「 | renamed r3_verify.first」を追記)。そのうえで、FULL の仕上げと同様に(g)、(h)、(i)をもう一度実行します(select 判定者は finalize 判定者の proof.md と、インデックスに記載された名前から最初の verify レポートを確認できます)。このフォールバックは最大 1 回まで適用され、2 回目の実行では、応答の 1 行目が何であっても(i)を最後まで実行します。 (e)Draft。 DRAFT BRIEF を使用する math-proof-judge を 1 つ実行します(state.md の {R}、{PARTIALS} は、仕上げが FULL かつ R ≥ ESC_ROUND の場合に DRAFT BRIEF の後に記載されたテキスト、それ以外は空(SHORT の仕上げ、または R < ESC_ROUND)です。R = 0 の場合は、brief の「final round's results」という節を「(ラウンド終了までに wave が完了しなかったため、summary と ledger に基づいて作業する)」に置き換えます)→ DIR/proof.md。追加クエリのルールが適用されます(Rules を参照。その再起動が発生した場合、それもこのステップに含まれます)。ステップ終了時に DIR/proof.md が存在しない場合、「DIR/proof.md was not written; write it now from the material named below.」という追加の第 1 段落を付けて draft 判定者をもう一度起動します。それでも存在しない場合は停止して報告します。 (f)Refine。 FULL の仕上げでは REFINE_STEPS 回実行します(ステップ名は refine_2、refine_3、…の順で、REFINE_STEPS 個)。SHORT の仕上げでは実行しません。各回で REFINE BRIEF を使用する math-proof-judge を 1 つ実行します(追加クエリのルールは各ステップにつき 1 回適用されます)。 (g)Select。 SELECT BRIEF を使用する math-proof-judge を 1 つ実行します → DIR/r3_q{k}.md を最大 MAX_COMMIT 個、および DIR/r3_verify.md をちょうど 1 個。実行後に DIR/r3_verify.md が存在しない場合、シェルを使って、何も再入力せずに、次を連結して作成します。「The document below is a draft proof. Check the argument step by step: for every inequality, interchange, cited result, and 'it follows that', ask whether it actually follows as written. List every error or gap in order of severity, and say explicitly whether the main claim is proved.」という行、空行、「## The draft proof」という行、空行、そして DIR/proof.md の内容。 (h)Commit wave。 DIR/r3_q{k}.md(SHORT の仕上げでは該当ファイルなし)と DIR/r3_verify.md をすべて 1 つの wave として実行します(この wave では screen ステップなし)。 (i)Finalize。 FINALIZE BRIEF を使用する math-proof-judge を 1 つ実行します({PARTIALS_FIN} は、仕上げが FULL かつ R ≥ ESC_ROUND の場合に FINALIZE BRIEF の後に記載されたテキスト、それ以外は空です)→ 最終版の DIR/proof.md。その後、単独チェックを実行します。grep -noE 'r[0-9]+_q[0-9]+|round[0-9]+_q[0-9]+|extra_q[0-9]+|r3_verify|[A-Za-z0-9_]+\.answer\.md|[A-Za-z0-9_]*summary\.md|synthesis\.md|ledger\.md|notes\.md|index\.md' DIR/proof.md || true (通常のファイル処理であり、数学の内容は読みません。出力がなければ proof.md に問題はありません)。何か出力された場合、proof.md はまだ、査読者が開けない実行ファイルを参照しています。FINALIZE BRIEF の前に次の第 1 段落を追加して finalize 判定者をもう一度だけ起動します。「DIR/proof.md still refers to run files (grep found: {一致箇所を最大 10 個、コンマ区切りで記載}). A referee reads proof.md alone and cannot open them. Rewrite DIR/proof.md so that every argument it relies on is written out in full inside proof.md itself, with no reference to any file in this directory.」。state.md に「standalone-check: resent」と記録し、その起動後に残った proof.md をそのまま受け入れます(チェックを繰り返しません)。 state.md を更新します(「phase: finished」)。次の内容をユーザーに返します。proof.md の場所、実行したラウンド数とループ終了の理由(スクリプトの verdict 行)、実行した worker クエリ数、回答された数、および partial で終わった数、目標が置き換えられた、または引き上げられたことがあったか(state.md から 1 行。DIR/result-so-far.md が存在する場合は、そこに worker が記述した以前の結果が保持されており、記録された目標変更の行までのみ確認済みで、proof.md とその Status セクションがこれに優先することを伝える)、そして finalize の応答にある判定者の Status 段落を引用します。数学の内容を自分で言い直したり評価したりしないでください。

全体を通して適用されるルール

  • すべての判定ステップとすべてのワーカーは、新しいサブエージェントの起動(Agent ツール)でなければなりません。subagent_type を明示的に設定してください。決して省略してはいけません。サブエージェントはこのプラグインに同梱されており、通常、エージェント一覧にはプラグインのスコープ付きの名前(math-proof:math-proof-judge、math-proof:math-proof-worker、math-proof:math-proof-worker-deep)で表示されます。席ごとに名前を決めてください。3つのそれぞれについて、エージェント一覧に短縮名(math-proof-judge、math-proof-worker、math-proof-worker-deep)があればそれを使い、なければスコープ付きの名前を使います。2種類の名前を混在させてもかまいません(ユーザーまたはプロジェクトの agents ディレクトリにある短縮名のコピーを使うと、その席の設定をユーザーが変更でき、その設定が優先されることを意図しています)。3つのいずれかがどちらの名前でも表示されていない場合は、このセッションのエージェント一覧に math-proof プラグインのサブエージェントがないことをユーザーに伝えてください。/plugin を開いて math-proof がインストールされ、有効になっていることを確認し、Claude Code を再起動して、同じ /math-proof:siege の行をもう一度実行するよう案内し、ラウンド1に進む前に停止します。各席で使った名前を state.md に記録してください。判定ステップでは math-proof-judge を使います。ワーカーは、ESC_ROUND より前のラウンドではラウンドのウェーブと再実行に math-proof-worker を使い、ESC_ROUND およびそれ以降のラウンドでは math-proof-worker-deep を使います。証明の後処理(追加クエリのウェーブ、コミットのウェーブ、r3_verify)では、ESC_ROUND 以降(state.md の R ≥ ESC_ROUND)にウェーブが実行されていた場合は math-proof-worker-deep を使い、それ以外は math-proof-worker を使います。選択は試行の進み具合についてのあなたの見解ではなく、ラウンド番号だけで決まります。以前のサブエージェントを再利用、再開したり、メッセージを送ったりしてはいけません。Agent ツールに model を渡してはいけません。判定役とワーカーはこのセッションのモデルで動作します。ウェーブ全体を1つのメッセージで起動し、ワーカーを並行して実行してください。サブエージェントをバックグラウンドで実行してはいけません。
  • 以下のブリーフとワーカープロンプトでは、DIR は実行ディレクトリの絶対パスを表し、その他の {角括弧で囲まれた} スロットは指定された値を表します。それらを置き換え、ほかは一字一句そのまま送ってください。ブリーフやプロンプトに、励まし、ヒント、問題についての意見、期限、結果の要約を追加してはいけません。
  • すべての math-proof-judge の起動に、固定の追加内容を適用します。ブリーフの後に空行を入れ、次の行を追加します。「Problem statement (for reference — DIR/problem.md is the authoritative text; go by the file wherever this copy differs or looks garbled):」その後に DIR/problem.md の内容全体を、バイト単位でそのまま続けてください(セットアップ中に読み込んだものです)。これは参照資料であり、判定役の最初のリクエストにすでに問題文が含まれるようにするものです。ブリーフの指示内容は変わらず、クエリファイルに問題文をコピーしてはいけないというブリーフのルールも引き続き適用されます。すべてのブリーフで指定されている DIR/problem.md が引き続き正式な本文です。正確に貼り付けてください。記憶を頼りにしたり、再入力したりせず、DIR/problem.md から読み込んだテキストを文字単位でそのままコピーします。
  • クエリファイル、回答ファイル(完成・未完成を問わず)、要約、台帳ファイル、notes.md、proof.md を自分で作成・編集してはいけません。自分が書き込むファイルは state.md、index.md、問題文のコピー、フォールバックの r3_verify.md、result-so-far.md のみです(最後の2つはコピーまたは連結だけで作成します)。それ以外では、手順で指定された場合に限りファイルをコピーまたは移動します(cp/mv:summary.md、および証明の後処理での r3_verify.first の名前変更)。回答ファイルについては、存在確認(test -s)以上の読み込みをしてはいけません。どの回答が完成しているかは、あなたではなく記録用スクリプト(後述の SCRIPT answers)が決定します。
  • ワーカープロンプトは常に次のとおりです。{Q} はクエリファイルの名前部分(例:round2_q3、extra_q1、r3_q2、r3_verify)、{PROBLEM} は DIR/problem.md の内容全体(バイト単位でそのまま)、{EARLIER} は空行です。ただし、このウェーブで最後に実行した answers が「partial」と報告したクエリを起動する場合は例外です。その場合は、このプロンプトの後に示す段落を {EARLIER} に入れ、その前後に空行を入れます。 「Task file: DIR/{Q}.md — read it first; the task concerns the problem stated below (DIR/problem.md holds the authoritative text of the problem; read it if anything in the copy below looks garbled). Write your answer to DIR/{Q}.answer.md as you go, and when you have finished, whatever the outcome, make the file's last line this end line, exactly: === END OF ANSWER {Q} === {EARLIER} Problem statement (verbatim, for reference): {PROBLEM}」 {EARLIER} が空でない場合、その内容は正確に次のとおりです。「An earlier worker's attempt at this task was cut off part-way; its unfinished answer is DIR/{Q}.partial.md — read it after the task file, use whatever in it you can check yourself, trust none of it as established, and write your own complete answer to DIR/{Q}.answer.md, ending with the end line above.」 終了行により、完成した回答と、(使用量上限、エラー、ターン上限などで)途中で打ち切られたワーカーの回答を区別します。記録用スクリプトが確認するため、あなたが確認する必要はありません。
  • クエリファイルのウェーブを実行するには、このウェーブで使う種類(最初のルールを参照。math-proof-worker または math-proof-worker-deep)のワーカーを各ファイルにつき1つ起動し、すべてを1つのメッセージで送ります。すべてのワーカーが応答してから(ワーカーがまだ動作中なら、ファイルへの書き込みも継続中です)、単独のコマンドとして SCRIPT answers DIR {Q1} {Q2} … を実行し、書き込んだり何かを起動したりする前に、その出力を読んでください。スクリプトは、あなたが内容を読まずに、回答ファイルのうちどれが完成しているかを判定し、クエリごとに1行を出力します。出力は「{Q}: answered」(DIR/{Q}.answer.md がそのクエリの終了行で終わっている。ワーカーが完了)、「{Q}: partial」(ワーカーは何かを書いたが完了していない。未完成ファイルは DIR/{Q}.partial.md に移動済みなので、.answer.md ファイルは常に完成した回答)、「{Q}: no answer」のいずれかです。続いて、「TOTAL (n queries): …」の行に3つの件数が表示されます(代わりに ERROR 行が表示された場合、コマンドを修正して安全に再実行できます。まず DIR、次に round2_q1 などの名前部分を指定します)。DIR/index.md にクエリごとに1行追加します。スクリプトの出力どおりに「{Q} | answered | 」、「{Q} | partial | 」、または「{Q} | no answer | 」とし、その後にワーカーの返信(回答ファイルの内容ではなく、要旨)の先頭300文字を追加します。改行はスペースに置き換えて、1行に収まるようにします。その後、ウェーブ内に answered でないクエリがある場合に限り、そのクエリごとに新しいワーカーを再起動します(一度だけ、すべてを1つのメッセージで起動します。answered のクエリは起動しません。partial のクエリには {EARLIER} 段落を含むプロンプトを使い、新しいワーカーに未完成ファイルを渡します)。すべてのワーカーが応答したら、ウェーブの全クエリ名を指定して SCRIPT answers をもう一度実行します(answered のクエリは変更されません)。各再実行対象の既存の index 行に(Edit ツールを使い、クエリごとに2行目は作成せず)「 | re-run: answered | 」、「 | re-run: partial | 」、または「 | re-run: no answer | 」を追加し、その後に前と同様に新しいワーカーの返信の先頭300文字を追加します。したがって index の行は「{Q} | status | abstract」となり、場合によっては「 | re-run: status | abstract」が続きます。再実行がある場合、適用される状態は再実行後の状態です。クエリが2回とも途中で打ち切られた場合は partial のままです。スクリプトは2つの未完成ファイルのうち長い方を DIR/{Q}.partial.md に残し、もう一方を同じ場所の DIR/{Q}.partial.prev.md に保存します。ワーカーの応答後、対応する answers の実行前に、そのクエリのワーカーを起動してはいけません。ウェーブの最後の answers 実行(すべてのクエリ名を対象とし、件数 n はウェーブのサイズと一致します)の TOTAL 行を記録してください。以下の FLOOR ルールと state.md で使用します。
  • このセッション中にユーザーが返答することはありません。続行方法を尋ねるためにターンを終了したり、確認を待ったり、何か問題が起きたからといって早期に停止したりせず、プロトコルが完了するか、以下のルールで停止するよう指定されるまで続けてください。サブエージェントがエラー、中断された結果、または空の返信を返した場合は、index.md / state.md に記録してプロトコルを続けます。ワーカーを1つ失うのは通常のことです。判定ステップがエラーまたは中断で戻った場合は、直ちに一度再起動してください。同じ判定ステップが連続して2回失敗した場合(エラーになるか、ファイルを1つも作成しない場合)は、停止して状況を報告します。ラウンドのウェーブが一度だけの再実行も含めて終了した時点で、最後の TOTAL 行の answered + partial が、スクリプトが WAVE の判定とともに出力した FLOOR の数を下回る場合(スクリーニング判定はこの数に含めません)は、停止して状況を報告してください。システム上の問題が起きており、続行しても判定ステップを無駄にするだけです。原因として最も可能性が高いのは、使用量上限または障害によってワーカーが打ち切られたこと、実行ファイルはそのまま残っていること、原因が解消した後に同じ /math-proof:siege の行をこのディレクトリで再実行すれば実行を再開できることをユーザーに伝えてください。(TOTAL 行の n がウェーブのサイズより小さい場合は、一部の名前部分だけで answers を実行しています。まず全件を指定して再実行してください。)追加クエリとコミットのウェーブには FLOOR はありません。
  • 追加クエリ:draft または refine のブリーフで許可されている場合、判定役は DIR/extra_q{k}.md という名前のファイルを、未使用の次の番号 k を使って最大3つまで作成できます。実行全体での上限は10です(DIR/extra_q10.md が存在したら、それ以上は作成できません。ブリーフにもその旨が記載されています)。判定役の返信に追加クエリファイルを作成したとある場合は、それらの存在を確認し、ウェーブとして実行します(回答は DIR/extra_q{k}.answer.md に保存されます。2回とも途中で打ち切られた場合は DIR/extra_q{k}.partial.md に保存され、どれが存在するかは index に記載されます)。その後、同じステップを一度だけ再起動し、冒頭に次の段落を追加します。「Your extra queries have been answered: read DIR/extra_q*.answer.md (the index says which exist). Finish the step now; do not write further extra queries in this step.」再起動したステップが追加ファイルを2回目に作成した場合は、未回答のままディスクに残します。
  • 各ステップの後に DIR/state.md を書き直してください。プロトコル、設定、現在のフェーズ、試行回数、およびステップごとに1行ずつ増えるログを記録します。各ラウンドの plan 行には、check コマンドに渡したウェーブ上限も記録します。また、各ウェーブの行には起動したワーカーの種類と最後の TOTAL 行を記録します(例:「cap 10, math-proof-worker-deep ×9, answered 8, partial 1, no answer 0」)。会話が要約された場合に参照できる唯一の記録です。現在の状況がわからなくなった場合は、state.md と ${CLAUDE_SKILL_DIR}/SKILL.md をもう一度読んでください。

計画ブリーフ(最大 {MAX_ROUNDS} ラウンド中の {r} ラウンド目;{CAP}、{HORIZON}、{CONCLUDE_RULE}、{ESC_SUMMARY}、{ESC_WAVE} は r に応じて変わります((a) および以下を参照))

ステップ:最大 {MAX_ROUNDS} ラウンド中の {r} ラウンド目を計画します。{HORIZON} ファイル:問題は DIR/problem.md、作業メモは DIR/notes.md、前ラウンドから引き継いだ要約は DIR/summary.md(第 1 ラウンドでは存在しません)、主張台帳は DIR/ledger.md(記録が行われるまでは存在しないか空です)です。前ラウンドの結果は、DIR/index.md の行でステータスが「answered」となっている ファイル DIR/round{r-1}_q*.answer.md(各行は「query | status | abstract」という形式で、ときに「| re-run: status | abstract」が続きます。その場合は再実行後のステータスが有効です。第 1 ラウンドでは該当なし)に加え、 存在する場合は DIR/extra_q*.answer.md です。ステータスが「partial」のクエリには、代わりにファイル DIR/round{r-1}_q{k}.partial.md があります。これは途中で打ち切られたエンジンのメモです。手掛かりや新たなクエリの土台となる情報を得るため、これも読んでください。ただし、そこに書かれた内容は何も確立されたものではありません。OPEN 行やクエリのきっかけにはできますが、それだけで PROVED 行にはできません(例外が 1 つあります。[GOAL] の主張、またはすでに提起された前の目標について、完全な証明または反証が書かれている場合は、以下の監査ルールにより、その証明はファイルが完成済みである場合とまったく同じように、監査ルール上「手元にある」とみなされます。また、監査ルールと結論ルールで求められる、確定した [GOAL] 行も記入してください。ロケーターには該当クエリの識別子(例:round3_q2)を使い、その後の検証クエリで確認します)。 (完成した結果ファイルはすべて、事務処理用の行「=== END OF ANSWER … ===」で終わります。この行は数学的内容ではありません。抜き出しや引用には含めないでください。)まず問題、メモ、要約、台帳、インデックスを読み、その後、前ラウンドの結果ファイルをそれぞれ一度、全文読んでください。

  1. まずスクリーニングを行います(第 2 ラウンド以降)。前ラウンドの結果ファイルを読む際に、それぞれがクエリに対する実質的な試みであることを確認します。拒否、空またはほぼ空のファイル、無関係な文章、別の問題への取り組みではないことを確認してください。そのラウンドのクエリごとに 1 行ずつ、DIR/judge/screen_r{r-1}.md に、正確に「round{r-1}_q{k}: OK」または「round{r-1}_q{k}: DEGENERATE: 理由を一行で」と記入します(回答なしのステータスのクエリには「DEGENERATE: no answer」とします。partial のクエリの .partial.md も完成済みファイルと同じ基準で審査します。未完成であること自体は degenerate の理由にはなりません)。DEGENERATE としたファイルは、以下のすべての作業で無視してください。 これはスクリーニングであり、採点ではありません。誤りがある回答、弱い回答、不完全な回答も OK です。

あなたは、難しい数学の問題に対する、複数ラウンドにわたる体系的な取り組みを指揮しています。各ラウンドで、非常に大きな思考予算を持つ深い推論エンジンに個別に送るクエリを作成します。結果はファイルとして返されるので、次のラウンドのクエリを作成する前に、そこから確立された内容を継続要約に反映します。これは最大 {MAX_ROUNDS} ラウンド中の {r} ラウンド目です。{HORIZON} {CONCLUDE_RULE}

次の 3 つを、順番に行ってください。

  1. 継続要約を更新します。DIR/round{r}_summary.md に一から書き直してください。このファイルは前の要約に置き換わり、以後のラウンド(および最終的な証明の組み立て)で、それ以前の内容を知る唯一の手段となります。そのため、引き継ぐべき関連事項はすべて記載してください。確立された内容と、それを示した結果ファイル(例:round2_q3)を記録します。有望な部分的進展、行き詰まった方針とその理由、現状から目標に至るまでの未解決の隔たりも記載してください。誠実に記述してください。過大な主張を含む要約は、その後のすべてのラウンドに悪影響を及ぼします。6000 語未満にしてください。次に、次の焦点を決めます。要約の最後に、次のラウンドでどこに集中すべきかを示す節を設けてください。最も強い部分的結果をさらに磨くのか、最も重要な未解決の隔たりを埋めるのか、この取り組みが依存している事柄を検証するのか、それとも行き詰まった方針を捨てて新たな視点を探るのかを記します。初期ラウンドでは通常、さまざまな独立した定式化やアプローチを試し、後期ラウンドでは通常、焦点を絞って取り組み、重要な手順を検証します。各ラウンドの判断はあなたに委ねられます。{ESC_SUMMARY}

  2. 主張台帳を更新します。要約と並行して、実行中は番号付きの主張台帳を管理し、各主張に PROVED、REFUTED、OPEN のいずれかを付けます。要約とは異なり、台帳は書き直しません。今回記入する行はそのまま追記されます(番号は自動で付与されます)。既存の項目を無効にできるのは、その番号を明記した RETRACT 行を追記する場合だけです。DIR/round{r}_ledger_block.md には、今ラウンドの新しい行だけを含めてください。各行は、「PROVED: 一文の主張 — locator」、「REFUTED: 一文の主張 — locator」、「OPEN: 一文の主張 — locator」(locator は round2_q3 のような結果ファイルの識別子)または「RETRACT 4: 項目 4 がもはや成り立たない理由を一文で」の形式とします。今ラウンドで確定または未解決となった、重要な根拠を伴う主張にはすべて行を追加し、ステータスが変わった主張には新しい行を追加します(同じ主張については最新の行が以前の行に優先します)。誤りと判明したものには RETRACT 行を追加してください。各行は一文にします。台帳全体は以後の各ラウンドおよび最終的な証明の組み立てにそのまま引き継がれます。この試みで折りたたんで消せない唯一の記録です。[GOAL] とする主要な目標を示す行には、ステータス語の直後に [GOAL] を付けます(「PROVED: [GOAL] …」、「OPEN: [GOAL] …」)。別個の検証クエリで完全な証明の連鎖を確認したことを記録する PROVED 行には [AUDIT] を付け、その検証クエリのロケーターと、証明対象の項目を「entry N」または「#N」として記載します。該当する行を追加する時点でタグを付けてください。第 1 ラウンドでは、[GOAL] 行をちょうど 1 つ記入します。問題で確定対象の主張が指定されている場合は、その主張、つまり問題で提示された主張全体とそのすべての部分を目標とします。課題が自由形式(提示された成果を改善、拡張または強化する、あるいはあるテーマについて重要な結果を見つける)であれば、この試みで確立できると判断する最も重要な結果を目標に選びます。正確に一つの命題を選び、確定するまでは OPEN として記録してください。(i)ステータス行。同じ主張について [GOAL] 行を追加できるのは、ステータスが変わるとき(OPEN → PROVED または REFUTED、あるいは検証クエリが証明の欠落を見つけて PROVED を RETRACT したうえで OPEN に戻すとき)だけです。また、完全な証明が結果ファイルに初めて含まれるラウンドで、検証クエリを同じステップで作成し、その回答が戻ったときには、すでに番号が付いた行を検証できるようにしてください。あるいは、以下の(iv)に従って再び戻る場合です。単に表現を変えるために追加してはいけません。[GOAL] 行のうち最新のものだけが有効であり、[AUDIT] 行は、それが証明する最新の [GOAL] 項目の番号を参照する必要があります(ブロック内の行には、DIR/ledger.md の最後の項目に続けてファイル内の順番で番号が付与されます)。(ii) 目標の変更。目標は固定ではありません。後の計画ステップで、新しい OPEN [GOAL] 行を記入して目標を変更できます。以後は、その目標が有効な目標となります(これは第 1 ラウンドで低い目標を選ぶ理由にはなりません。第 1 ラウンドの目標は上記のとおり選んでください)。このブリーフ全体を通じて、「[GOAL] 行」と「[GOAL] の主張」は、最新の有効な [GOAL] 行とその主張を指します。目標を新しく設定する理由は 2 つあります。目標が誤り、不適切、またはすでに知られていたと判明した場合、あるいは問題で提示された主張よりも狭い、または異なると判明した場合は、目標を置き換えます(古い [GOAL] 行を RETRACT します。証明済みで証明が有効なら、その内容を通常のタグなし PROVED 行として再記録してから、新しい目標を記入します)。この場合、問題で提示された主張を新しい目標にします(証明済みの狭い目標であっても、引き上げるのではなく置き換えます。問題で主張が指定されている場合、この実行の判定はその主張について行うためです)。自由形式の課題で第 1 ラウンドに独自に選んだ目標が反証された場合は、それを置き換えて続行します(引き上げた目標については(iii)を参照)。REFUTED [GOAL] 行によって実行を終了するのは、問題でその主張自体が提示されていた場合に限ります。あるいは、現在の目標が PROVED となり、より重要な結果が残りラウンドで到達可能に見える場合は、目標を引き上げます。より強い命題、または証明済みの内容の一般化を、新しい OPEN [GOAL] 行として記入します(引き上げる目標は第 1 ラウンドで選ぶ目標と同じ基準を満たす必要があります。つまり、この試みで確立できると判断する正確な命題であり、誤り、不適切、またはすでに知られていると分かっているものではありません)。引き上げは必ず OPEN 行として記録します。結果ファイルで実際に証明された範囲を超える主張を PROVED [GOAL] 行にしてはいけません。問題で提示された主張をそのまま証明できた場合、引き上げる目標はありません。結論を出してください。(iii) 引き上げ後も維持される内容。目標を引き上げた場合、証明済みの目標やその [AUDIT] 行は RETRACT しないでください。有効な項目として残ります。引き上げた目標を達成できなかった場合、最終文書ではその結果を提示します。引き上げた目標の証明に欠落があると検証クエリで判明した場合は、その PROVED [GOAL] 行を RETRACT してください。証明の検証に失敗した PROVED [GOAL] 行を有効なままにしてはいけません。その後、(ii)に従ってどの命題を目標とするか改めて判断し、以前の目標に戻る場合は、それを最新の OPEN [GOAL] 行として記入し、未解決の箇所に照準を合わせます。引き上げた目標の REFUTED は実行全体の判定ではなく、その反証に検証クエリは必要ありません(以下の監査ルールは、実行の結論として採用する目標を対象とします)。反証したファイルを記載した「REFUTED: [GOAL] …」行を記録し、その下に(iv)のとおり、証明済みの目標を再度記入して、それを結論とします。目標を引き上げるかどうかは判断事項であり、義務ではありません。より重要な結果が明確に到達可能でなければ、前述の結論ルールに従って証明済みの目標について結論を出します。また、引き上げた目標を狙った最初の 2 波(引き上げたラウンド自身の波が第 1 波)で進展がなければ(その目標の証明も、新たな証明経路も得られなければ)、次の計画ステップでは、すでに証明済みの目標に戻って結論を出します。戻る場合は、要約の連鎖・進展ルールと以下のエスカレーションルールよりも優先されます。これらのルールは、目標としている間に停滞した命題に波を向けるためのものです。すでに証明済みの目標に戻るステップでは、監査ルールでその目標に必要とされる検証クエリ以外のクエリを作成してはいけません(監査の波を 1 回行った後、結論を出します)。すでに証明済みの目標に戻る場合を除き、証明が難しいからという理由で目標をより弱いものに変更してはいけません。到達できなかった目標に向けて確立された内容は、証明文書作成の各ステップで、そのまま提示します。採用しなかった、より強い結果や追加の結果は、通常の PROVED/OPEN 行として残し、証明の「その他のアプローチ」節に記載します。(iv) 再び戻る場合。以前に証明した目標に戻る場合(引き上げた命題に成果がなかった場合)、このラウンドのブロックに、その目標を「PROVED: [GOAL] …」という行で再記入します。以前の項目を「entry N」または「#N」として参照し、ブロック内に他の [GOAL] 行がある場合はその後に配置して、最新の行にしてください(番号はファイル内の順に割り当てます)。その下に、認証を [AUDIT] 行として再記入します。各行には、以前と同じく検証クエリのロケーターを記載し、新しい行の番号を同じ形式で参照します(数えてください。DIR/ledger.md が項目 23 で終わり、目標の再記入がブロックの 2 行目なら、それは項目 25 です)。以前の項目を参照する目標行なら検証クエリ 1 つで十分です。それ以外の場合は、別々のクエリによる 2 つの検証が必要です。その後、結論ルールに従ってください。確定、未解決、変更または撤回された主張がない場合は、ファイルを空のままにしてください。

  3. 次のラウンドのクエリを作成するか、結論を出します。手元の資料が目標を完全に確立している場合に限り、DIR/round{r}_DONE.md に、その内容を確立している箇所を示す 1 行を記入し、クエリは作成しません(このステップで目標を引き上げた場合は、その目標に対する波を作成します。目標の引き上げと同じステップで DIR/round{r}_DONE.md を作成してはいけません)。それ以外の場合は、DIR/round{r}_q1.md、DIR/round{r}_q2.md、… に、選んだ対象を狙うクエリファイルを {CAP} 個まで(1 個以上)作成します(番号は連番とします)。[GOAL] 行が OPEN の間は、並列クエリは容易かつ独立に実行できるため、予算の大部分を使うことを優先し、同じ試みを言い換えるのではなく、真に異なる方法で対象に取り組ませてください。[GOAL] の主張の完全な証明(または反証)が手元にある場合は、波の規模を縮小します。以下の監査ルールで必要とされる検証クエリに加えて、最終的な証明文書に必要な内容(系の完全な記述、引用されただけの補題の証明、独立した第 2 の証明など)を狙うクエリを最大 2 つ作成します。このステップで目標を引き上げた場合(項目 2)、波は縮小しません。証明済みの連鎖に対する検証クエリは送信し、後のラウンドでその認証が返ってきた際には、目標がすでに変更されていても、ロケーターと認証対象の PROVED 項目の番号を記載した [AUDIT] 行として記録します。残りのクエリは上限まで、新しい OPEN [GOAL] 行を対象に作成します。このブリーフに以下のエスカレーションルールが含まれる場合、波のその部分は、証明が手元にない引き上げ後の主張を [GOAL] として、そのルールに従います。まず、引き上げ後の主張について、要約に「連鎖と未解決の命題」節を記載します(要約ルール(iii)。まだ何も帰着されていない場合は、引き上げた主張そのものを未解決の命題とし、その OPEN [GOAL] 行を台帳の項目として扱います)。次に、エスカレーションルールに従って、その部分の波を作成します。各クエリは自己完結している必要があります。推論エンジンに渡されるのは、そのクエリファイルと完全な問題文だけで、要約、台帳、他の結果、別ラウンドの内容は渡されません。そのため、クエリが以前の結果や部分的な議論を土台にする場合は、必要な内容をクエリ内に含めてください(長い文章は再入力せず、シェルを使って回答ファイルから抜き出してください)。問題文自体をクエリにコピーしてはいけません。 対象選択ルール(毎ラウンド適用)。作成するクエリのうち少なくとも半数(端数は切り上げ)は、この実行で特定した未解決の問いに取り組む必要があります。対象には、結果ファイル内で示された未解決の問い、台帳の OPEN 項目、要約に記載された未解決の隔たりが含まれます。そのようなクエリは、1 行目を正確に「kind: attempt」とし、対象とする具体的な未解決の問いを本文中に記してください。attempt クエリは、その問いを解決する(証明、反証、またはそれより厳密に易しい問いへ帰着させる)ことを試みるものです。概観するだけ、既知の基礎事項を再導出するだけ、または文書を整えるだけではいけません。問いが「established: open」であるという判定(あるいは目標が既知の到達範囲を超えているという判定)は最終的な結論ではありません。それを後のラウンドで確定済みとして引き継いではいけません。再び未解決として扱い、直接解決を試みるクエリを作成してください。 監査ルール(毎ラウンド適用)。手元にある結果ファイルが [GOAL] の主張、またはこのステップ以前もしくは今回のステップで引き上げて離れた目標(引き上げた目標の反証は除きます。項目 2(iii)を参照)の完全な証明(または反証)を示しており、まだ 2 つ未満の検証クエリしか認証していない場合は、このラウンドで不足している数(2 つ、または 1 つ)以上のクエリを、その証明の独立した検証クエリにします。完全な証明を示す結果ファイルが複数ある場合は、最も完全なものを選び、その同じ証明について 2 つの検証クエリを送ります。各検証クエリには、完全な論証を逐語的に含めます。回答ファイル(上記のファイル一覧に示した例外に該当する場合は partial ファイル)から、シェルを使ってクエリファイルを組み立ててください(cat、sed を使用)。再入力や言い換えはしないでください。そして、すべての推論を段階ごとに確認し、論証がそのままの形で主張を証明しているかどうかについて、明示的な判定で締めくくるよう求めます。これらも attempt クエリとして数えます(1 行目は「kind: attempt」とし、監査対象の [GOAL] 項目を記載します)。2 つの認証でこの条件を満たします。2 つの検証では確認できない点を調べる場合に限り、3 つ目を追加してください。この認証が肯定的な結果となった場合は、ロケーターを記載し、認証対象の [GOAL] 項目の番号を明記した PROVED [AUDIT] 行として記録します(目標がその後引き上げられていても、確定したその目標の行を対象とします)。そのうえで台帳が条件を満たしたら(上記参照)、結論を出してください。{ESC_WAVE} 検索ルール。継続要約は圧縮された記録なので、結果の内容を省略したり、逆に伝えたりすることがあります。以前の結果に依拠したり、それと矛盾したりする場合は、要約の書き直し、台帳の行、対象の選択、結論の判断のいずれであっても、まずその結果の回答ファイルを読み、その実際の記述に基づいて作業してください。要約の言い換えに依拠してはいけません。

最後に DIR/notes.md を書き直し、150 語未満で、結論に至ったかどうか、クエリファイルの数、そのうち attempt クエリの数、対象を一文で回答してください。このラウンドで目標を置き換えた、引き上げた、または以前の目標に戻った場合(項目 2)は、150 語に含めない追加の一文を記述し、「Goal change:」で始めてください。その文には、3 つのうちどれか、変更前の目標と変更後の目標(それぞれを短く記述)、証明済みの結果がある場合はその台帳項目番号と、これまでにそれを認証した検証クエリの数を含めます。目標を引き上げた場合は、その結果の完全な証明を含む回答ファイルのフルパスも記載してください(形式:「Goal change: raised — entry N, proved in DIR/roundK_qJ.answer.md (certified by M verify queries so far), is …; the goal is now …」)。 {CONCLUDE_RULE} は、r < MIN_ROUNDS の場合、厳密に次のとおりです。「claims ledger に見出しの目標が確定済みとして記録された時点、つまり [GOAL] タグが付いた PROVED または REFUTED の行(「PROVED: [GOAL] …」)があり、さらに [AUDIT] タグが付いた PROVED の行が少なくとも2行あれば、ラウンド {MIN_ROUNDS} より前でも、このラウンドで結論を出せます。各 [AUDIT] 行は、完全に記述された証明チェーン(スケッチや概要ではありません)を確認した個別の verify クエリが返す認証です。クエリのロケーター(例:round3_q2)を記し、[GOAL] 行、またはその行が引用する行を、ledger の ID を「entry 12」または「#12」と記して引用する必要があります。少なくとも1つの [AUDIT] 行は、[GOAL] 行そのものを引用しなければなりません。ledger が条件を満たしたら、このステップでは次の2つのうちどちらかを選びます。結論を出すか、目標を引き上げ(いつ、どのように行うかは以下の項目2を参照)、引き上げた目標に向けた wave を作成します。{MIN_ROUNDS} に達することや、仕上げを目的として、さらに wave を実行してはいけません。仕上げは、この後の証明を書くステップで行います。行には出てきた時点でタグを付けてください。ledger がまだ条件を満たしていない場合は、wave を作成します(verify クエリを含めなければならない場合については、以下の監査ルールを参照)。」 — r ≥ MIN_ROUNDS の場合、厳密に次のとおりです。「このラウンド以降は、手元の資料で [GOAL] の主張が完全に立証されたら、いつでも結論を出せます。ただし、完全に記述された証明が手元にあり、verify クエリがまだ2つ未満しか認証していない場合は、以下の監査ルールを今ラウンドも適用します(監査 wave を1回実行してから結論を出します)。また、そのような証明が手元にある場合、このラウンドの ledger ブロックには、通常の形式の「PROVED: [GOAL] …」(または「REFUTED: [GOAL] …」)という確定済みの [GOAL] 行が、ステータス語とタグの間に何も入れずに、verify クエリを作成するのと同じステップで、すでに記載されている必要があります。まだ認証されていないこと自体に印を付ける必要はありません。認証状況は [AUDIT] 行に記録されます。[GOAL] の主張が立証されたら、(監査ルールが適用される場合は監査 wave の後に)結論を出すか、目標を引き上げます(以下の項目2を参照。引き上げる場合、監査を待つ必要はありません)。同じステップで両方を行ってはいけません。目標を引き上げるステップでは、DONE ファイルを書き込みません。引き上げた目標は、結論を出すのではなく、wave によって確定するためです。前のラウンドで目標を引き上げており、引き上げた命題がまだ導かれていない場合は、項目2(iv)の説明に従って、すでに証明された目標を最新の [GOAL] 行として再記載し、結論を出してもかまいません。最終ラウンドでは、ラウンドがそのまま終わるのを待つのではなく、この方法を取ってください。」

{HORIZON} は、r ≤ MAX_ROUNDS−2 の場合は空です。r = MAX_ROUNDS−1 の場合は、厳密に次のとおりです。「したがって、この後に実行できるラウンドは最大1回です。」r = MAX_ROUNDS の場合は、厳密に次のとおりです。「したがって、これが最終ラウンドです。このラウンドのクエリが返す内容は、そのまま証明を書くステップに進み、それに対応するための次のラウンドはありません。」(先頭の空白に注意してください。ブリーフ内の {MAX_ROUNDS} は、各ラウンドにおける MAX_ROUNDS 設定の数値です。) {ESC_SUMMARY} は、r < ESC_ROUND のとき空です。r ≥ ESC_ROUND のときは、次のとおりです(先頭の空白も含みます)。 " このラウンド以降、要約にはさらに次の4つの規則が適用されます。規則(iii)ではあなた自身の数学的考察が求められるため、作業を中断されると、書き残されていない内容は失われます。先に、引き継いだ内容と(i)~(ii)を要約ファイルに書き、その後で(iii)に取り組み、要約を拡充してください。(i)既知の結果:この名前のセクションを設け、問題全般(すべてのパラメーター)に関する定理である証明済みの台帳項目、[GOAL] の主張を名前の付いたより簡単な、または古典的な命題へと正確に言い換えたり帰着させたりしたもの、あるいは自然な特殊ケースの完全な解決を、各項目の所在情報とともにすべて列挙します。それだけでは目標を達成できない場合も含めます。このセクションから項目を削除してはいけません(代わりに「現在の主線では未使用」と記してください)。目標に到達できなかった場合、最終文書はこれらを軸に構成されるためです。(ii)行き詰まり:ある経路を行き詰まりとするのは、特定の主張が反証され、その反証を示した結果ファイルがある場合に限り、まさにその形で記録します。障害を報告した結果ファイル、1つの仮定形または1つの候補の範囲内で探索に失敗した報告、あるいは経路が目標の一部にしか到達しないとの報告は、その候補を打ち切るだけであり、経路全体を打ち切るものではありません。そのような経路は未解決の課題の下に「保留、未反証」として列挙し、再検討できる状態にしておきます。(iii)論証の連鎖と未解決の命題。まず、[GOAL] の主張について完全な証明または反証が文書として手元にあるかを判断します。前のラウンドの未解決の命題を、そこに記されたとおりに証明する結果ファイルがあり、その連鎖にそれ以上のものが不要なら、それが完全な証明または反証です。その場合、今ラウンドの台帳ブロックに [GOAL] の行を証明済み(反証の場合は反証済み)として記録し、その連鎖で用いる項目を番号で引用して、新しい証明の所在情報を示します。また、監査規則の検証クエリーを、連鎖全体を含む形で構成します。つまり、引用した項目の論証と新しい証明を、それぞれの回答ファイルから抜き出し、前のラウンドの要約に記載された連鎖の導出に従ってつなぎ合わせます。これ以外の方法でも完全な証明または反証が手元にある場合は、(iii)の残りと(iv)全体を省略します。それ以外の場合は、「論証の連鎖と未解決の命題」という見出しのセクションを要約に設け、毎ラウンド書き直し、次の4つのラベル付き部分を含めます。

連鎖:[GOAL] の主張(または、追求している方針が反証の場合はその否定。以下の「未解決の命題の証明」もそれに応じて読み替えてください)が、すでに証明済みの結果(台帳番号で引用し、命題のみを記載)と、まだ証明されていない追加の命題ただ1つから、どのように導かれるかを示します。導出は段階を追って書き、引用した項目とその1つの命題の証明を持つ読者が、完全な証明を得られるようにしてください。資料から目標を単一の命題にまで帰着できない場合は、主線が次に必要とする最も強い中間命題を未解決の命題とし、それを得た後に何が残るかを連鎖に記してください。

未解決の命題:その命題を、完全かつ自己完結した形で記します。すべての量化子、定義されるすべての対象、および利用する可能性のある問題の仮定をすべて明記します。実際に必要な仮定を取り除いた命題は偽になり、その反証によって妥当な主線が損なわれるおそれがあります。その命題には独自の仮定を含めてもかまいません。たとえば、対象の一部やパラメーター範囲の一部への制限を含める場合は、そうした仮定の外にあるすべての事柄がすでに解決済みであることを、証明済みの項目を引用して連鎖で示す必要があります。その証明を得ても問題で許される対象の一部が未解決のまま残る命題は、特殊ケースであって未解決の命題ではありません。連鎖を完成させる命題の中から、最も簡潔で具体的なものを優先します。初めて提示したときと、その表現を変更するたびに、台帳へ未解決の行として記入し(所在情報には、N を今ラウンドの番号として roundN_plan と記します)、置き換えられる表現の未解決の行も撤回します。これにより、後のラウンドやクエリーで参照できます。

成立すると考える理由:なぜ成立すると考えるのか、またどのような論法で証明できそうかを、あなた自身の考察として最大15行で示します。この数学的考察はあなた自身で行ってください。どのような種類のものであれ、実現につながりそうな候補となる仕組みが見えたら、それを厳密に述べます。この段階で生まれたあなたの予想をエンジンが証明または反証することも、成果の中で特に有用なものの1つです。

これまでに試したこと:この命題または以前の表現についてすでに実行したクエリーを、1クエリーにつき1行で記します。所在情報、そのクエリーが試みたアプローチ、および得られた結果(特殊ケースの証明、同値な言い換え、障害、何もなし)を記してください。同一タスクの重複は1行にまとめます。このように列挙したアプローチは試行済みとして扱います。

(iv)進捗の判定。対象セクションの冒頭で、直近2ラウンドに連鎖の進捗があったかを示します。進捗として数えるのは、未解決の命題の証明、[GOAL] の主張の証明、仮定が許すすべての対象に成り立ち、連鎖を短縮する新たな証明済みの結果、または未解決の命題を厳密により簡単なもの(単に範囲を狭めたものではない)に置き換え、連鎖を改めて導出した場合のみです。未解決の命題の難所が未解決のままで、対象の一部についてさらなる結果を得て命題の範囲を狭めただけの場合や、同値な言い換えをした場合は、(i)に記録しますが、この意味での進捗とは見なしません。進捗がなかった場合は「主線は停滞 — 全称的な進捗なし」と記し、自分の考察または分解について前のラウンドと異なる点を1行で述べます。そして、別の特殊ケースを始めたり、幅を広げるために別の経路へ移ったりしてはいけません。第2項(iii)によって、すでに証明済みの目標に立ち戻って結論を出す場合を除き、次の波は、以下の終了規則に従って未解決の命題そのものへ向かいます。(iii)における自分の考察を変える必要があります。同じ命題に対する別の仕組みを考えるか、異なる未解決の命題を導くために連鎖を別の方法で分解してください。結果ファイルが未解決の命題を記載どおりに反証した場合、その反例の属するクラスを除外して救済してはいけません(証明済みの項目がすでにそのクラスを解決しており、連鎖がそれを示している場合を除きます)。修正した未解決の命題を述べて連鎖全体を改めて導出するか、その行を(ii)に従って行き詰まりとして記録し、次に有望な行について連鎖を構築してください。このラウンド以降、「検証」を目標とするのは、監査規則の目標監査と、終了規則の項目(c)が認める1つの連鎖チェックに限ります。" {ESC_WAVE} は r < ESC_ROUND の場合は空です。r ≥ ESC_ROUND の場合は、次のとおりです(先頭のスペースを含み、{CAP} は他の箇所と同様に置換します)。 " エスカレーションルール(このラウンドと、それ以降のすべてのラウンドに適用されます。[GOAL] の主張について完全な書面による証明または反証が得られるまで続きます。証明済みの欠落した命題によって連鎖が完成した場合を、ケースサマリールール (iii) が説明している場合も含め、いったんその証明または反証が得られたら、監査ルールと上記の縮小されたウェーブが適用され、以下の (a)〜(c) は無視されます)。このラウンドで回答するエンジンには、最初のラウンドよりはるかに大きな思考予算があり、ウェーブには最大 {CAP} 件のクエリを含められます。その大半を使い、調査や、単に対象範囲を広げることではなく、連鎖で欠けている命題を完全な形で述べたうえで、その命題に費やしてください。(a) すべてのクエリは攻撃を試みます。欠けている命題、[GOAL] の主張そのもの、またはその答えによっていずれかが解決するか、厳密に範囲が狭まる問いに取り組みます(対象の一部についてのみ解決しても、範囲が狭まったことにはなりません)。[GOAL] の連鎖を完成させない結果の書き上げ、推敲、再導出、検証にクエリを費やさないでください。ラウンド後の証明作成ステップでは、それぞれ独自のクエリ予算を使ってこれらを行うためです。したがって、ラウンド内の検証クエリは、監査ルールのもの(証明された後に引き上げられた目標を認証する検証クエリも監査ルールに含まれます)と、(c) で許可される連鎖チェック項目 1 件だけです。エンジンに、[GOAL] の主張やその他の何かについて、文献から証明を思い出したり再構成したりするよう求めるクエリは出さないでください。エンジンには参照できるライブラリがなく、そのようなタスクでは推論材料を何も得られません(攻撃の中で既知の定理に言及するのは別の話であり、問題ありません)。(最終の 2 ラウンドに限り、このブリーフの冒頭にある「Step: plan round …」の行で、「one further round」または「the final round」という文言を使ってその旨が明示されます。どちらの文言もない場合は、最終の 2 ラウンドには該当しません。この場合、最大 2 件のクエリを、最終文書に掲載する既存の結果の検証、または完全な書き上げに充ててもかまいません。)(b)締めくくりルール。 欠けている命題だけについて、完全な証明、または明示的な反例を求めるタスクファイルを 1 つ作成し、以下を含めてください。サマリーに記載されている命題を一字一句そのまま記載すること、それが依拠できるすべての先行結果を、回答ファイルから証明も含めて完全な形で挿入すること(cat、sed を使い、決して言い換えないこと)、その命題から [GOAL] を導く連鎖の導出(エンジンが命題の目的を理解し、導出自体に欠陥があれば指摘できるようにするため)、命題が成り立つと考える理由のスケッチ(エンジンが自由に破棄できる提案として示すこと)、そして、命題が対象とする一部のケース(対象の部分クラス、またはパラメーターの一部の範囲)についてのみ証明しても問いへの回答にはならないが、それが見つかったものすべてであれば報告すべきである、という明示的な文を含めます。このラウンドのクエリファイル q1(前述のファイルの最初のもの)として保存し、バイト単位でそのまま(cp)q2 と q3 にコピーします。3 つのエンジンが同じ命題に独立して取り組みます。ここでは、適切に定式化された 1 つの命題に対する独立した試みのほうが、3 つの命題にそれぞれ 1 回ずつ取り組ませるより価値があります。同一のコピーは意図されたものです(1 つの試みを言い換えることを禁じる上記の指示は適用されません)。3 件すべてを試行クエリとし、最初の行を 'kind: attempt' にして、取り組む未解決の問いとして欠けている命題を指定します。(c) 残りのクエリも、上限の大半を使って、欠けている命題に割り当てます。それぞれ単独で完結させ(下記に特記がない限り、同じ挿入内容を含めます)、締めくくりタスクのバイト単位のコピー(許可されています。独立した試みがもう 1 件増えるため)か、締めくくりタスクとは本質的に異なるもののいずれかにします。異なるクエリには、「Tried so far」に記載されていない、明示したアプローチによる攻撃を含めます(タスク内でそのアプローチを明記してください。エンジンが別のアプローチを取る場合は、その理由を述べるようにします)。または、返された部分的な結果を挿入したうえで、その結果から続ける、記載済みのアプローチを含めます。または、スケッチの中で最も難しい単一のステップを切り出し、単独で完結する主張として提示します。または、結果ファイルが命題に対する障害として挙げた 1 つの事項を、克服すべきもの、あるいは反例へと絞り込むべきものとして提示します。最初のラウンドでは欠けている命題を提示します。また、その文言が変更された場合も毎回、これらのクエリのうち 1 件では、記載どおりの命題に対する反証を試みます。具体的な構成を示すか、その命題から既知の偽である結果を導くことで反証してください。同じ欠けている命題がすでに 2 つの先行ラウンドで攻撃されている場合、これらのクエリのうち 1 件には命題と、引用された項目の主張のみを記載し(証明とスケッチは含めません)、まず、その命題によって [GOAL] が完成することをエンジン自身に導出させたうえで、列挙済みの試みが使っていない最初の一手で攻撃するよう求めます。導出が成り立たない、または命題がもっともらしくないと判断したエンジンは、その旨を述べます。これはサマリールール (iv) に基づいて対応すべき結果です。ウェーブ内のクエリのうち、他の主経路から派生しない経路(サマリールール (ii) のもとで、反証ではなく保留された経路)に割り当てられるのは最大 2 件です。または、そのうち最大 1 件を、別のクエリでまだチェックされていない、連鎖が依拠する証明済みのステップ 1 つのチェックに充てます。これらはすべて試行クエリとし、最初の行を 'kind: attempt' にします。"

ドラフト概要

ステップ:証明の草稿。ファイル:問題はDIR/problem.md、作業メモはDIR/notes.md、この試みで明らかになったことすべての作業中の要約はDIR/summary.md、主張の台帳はDIR/ledger.md、最終ラウンドの結果は、DIR/index.mdでansweredとマークされ、DEGENERATEではない最新のDIR/round{R}_q*.answer.mdファイルです。それ以前のすべてのラウンドの結果ファイルとDIR/extra_q*.answer.mdは、ファイル名を参照して確認できます(インデックスでクエリがpartialとされている場合のDIR/…_q{k}.partial.mdファイルは、途中で打ち切られたエンジンの未完成かつ未検証のメモです。手がかりにすぎず、そこに記された内容は何も確立されていません。また、各完成ファイルを閉じる「=== END OF ANSWER … ===」行は記録管理上のものであり、数学的な内容ではありません)。 まず問題、メモ、要約、台帳、最終ラウンドの結果を読んでください。

あなたは、難しい数学の問題に対する構造化された複数ラウンドの試みを指揮しています。各ラウンドは終了しました。 今すべきこと:目標に至る最も有力な道筋、つまりこの試みで見つかった最も完全な議論を、議論の全容を明記してDIR/proof.mdに書き、{PARTIALS}を加え、記録に値する他のすべての道筋について短く触れ、未解決のギャップがあれば正直に記してください。明確にギャップと示すほうが、取り繕うより価値があります。最新の[GOAL]行がPROVEDではない場合、またはPROVEDでも2つの[AUDIT]行による検証がなく、記述した証明が自分で確認しても成立しない場合に、台帳に、過去に達成された後で引き上げられた別の主張(該当するものが複数ある場合は最新のもの)について、効力のあるPROVED [GOAL]行があるなら、その証明済みの目標をproof.mdの主張の中心にしてください。それを文書の定理として述べ、その証明を、台帳が指定する結果ファイルから完全に書き起こしてください(台帳が指定するファイルが.partial.mdファイルの場合は、その主張を含み、回答によって検証されたverifyクエリファイルから本文を取得してください)。それは副次的な結果ではありません。引き上げられた目標はその後に、試みた主張として記し、それに向けて確立されたことを示してください。Statusセクションでは、それぞれがどちらに当たるかを明記してください。具体的な計算で手順を確認または否定できる場合は、必ずpython3を使ってください。候補となる等式を例で確認する、定数を検証する、主張された反例を数値的に試す、といったことを行ってください。思い込みより検証を優先してください。証明の要となる点を、的を絞った少数の高度な推論クエリで解決できる場合は、未使用のDIR/extra_q{k}.mdファイルを次のファイルとして作成してもかまいません(このステップでは最大3件、DIR/extra_q10.mdがすでに存在する場合は作成しないでください)。各ファイルは単独で内容が分かるようにしてください。エンジンにはそのファイルと問題文しか渡されないため、必要な前提はその中に記載し、問題文自体はコピーしないでください。作成した場合は、返信でその旨を伝えてください。その後、回答を受け取り、もう一度呼び出されます。このステップでは、必ずDIR/proof.mdを書いてください。DIR/notes.mdを書き直してください。150語未満で返信してください。

{PARTIALS}は、SHORT末尾の場合、およびR < ESC_ROUNDの場合は空です。FULL末尾でR ≥ ESC_ROUNDの場合は、次の文言がそのまま入ります(先頭のスペースも含む)。「また、最新の[GOAL]行が検証されていないため、台帳または要約にある、自然な特殊ケースを解決する結果、目標を正確に言い換えるまたは目標を簡約する結果(定理として述べること:「…という条件のもとで、すべての…について主張が成り立つ」)、あるいは目標またはその未解決部分を名称のある既知の命題と結び付ける結果のうち、PROVEDとされたすべての結果についても、証明を本文中にすべて書き起こすこと(引き上げられた目標に関する以下の文が当てはまる場合は、以前に証明された目標の定理の後、未解決部分の記述より前に置く)。最も一般的なものを最初に述べる。試みた目標を解決できなかった場合、査読者は、実際に確立された簡約と部分結果によって評価します。したがって、これらは本文を構成するものであり、補足メモではありません。」

再検討ブリーフ(ステップ名 {S} = refine_2、refine_3、…の順)

ステップ:{S}。ファイル:問題は DIR/problem.md、作業メモは DIR/notes.md、現在の草稿は DIR/proof.md、結果ファイルは DIR/round*_q*.answer.md(各ラウンドの結果)および DIR/extra_q*.answer.md で、そのステータスとともに DIR/index.md に一覧されています(ステータスが「partial」のクエリは、代わりに DIR/…_q{k}.partial.md があります。これは途中で打ち切られたエンジンの未完了かつ未検証のメモであり、結果ではなく手がかりです。 また、各完了ファイルを閉じる「=== END OF ANSWER … ===」の行は、数学的な内容ではなく管理用の記録です)。主張の台帳は DIR/ledger.md、作業中の要約は DIR/summary.md です。 まず問題、メモ、草稿を読んでください。結果ファイルは必要に応じてファイル名を指定して参照してください。

あなたは難しい数学の問題に対する、構造化された並列試行の合間にいます。このステップの仕事は、proof.md を厳密に改善することです。弱い箇所を再導出し、敵対的な査読者のように誤りを探し、依拠する具体的な計算上の主張をすべて python3 で検証してください。重要な論理の穴を埋めるために、対象を絞った深い推論クエリが1つ必要なら、次に使われていない DIR/extra_q{k}.md として記述できます(このステップでは最大3つ。DIR/extra_q10.md がすでに存在する場合は作成しないでください)。クエリは自己完結させてください。エンジンに渡されるのはそのファイルと問題文だけなので、前提となる内容をインラインで含め、問題文自体はコピーしないでください。作成した場合は、返信でそのことを述べてください。その後、受け取った草稿を最初に DIR/judge/{S}_previous_proof.md として保存してから、DIR/proof.md を全文書き直してください。未解決の点は正直に明示してください。ごまかすより、明確に穴として示すほうがよいです。DIR/notes.md も書き直してください。返信は150語未満にしてください。

ルート選択

ステップ:コミット段階のルート選択。ファイル:問題は DIR/problem.md、作業メモは DIR/notes.md、草稿は DIR/proof.md、最終ラウンドの結果(および必要な以前の結果ファイル)は DIR/index.md に記載されています(クエリのステータスが「partial」の場合、エンジンが途中で打ち切られたことによる未検証のメモのみが DIR/…_q{k}.partial.md にあります)。主張の台帳は DIR/ledger.md です。

あなたは難しい数学の問題に対する、構造化された並列試行を行っています。証明草稿と、取り組みの全結果があります。あなたの仕事はプロトコルのコミット段階です。目標に向けた具体的な道筋(名前の付いた補題の連鎖や、特定の構成)がある結果はすべて、最大限の思考予算でコミットクエリを作成してください:「Route: [そのルート]。Write the full rigorous proof.」。さらに、草稿の証明を段階ごとに検証するクエリを1つ作成してください。(目標を証明できたものの、その後に引き上げられた目標は証明できなかった場合、草稿の主張は証明済みの目標です。引き上げられた目標に向けた具体的なルートもコミットできます。) コミットする価値のあるルートを最大 {MAX_COMMIT} 個まで選んでください(それより少なくてもかまいません。具体的なものがあるルートだけを選んでください)。各ルートについて、クエリを DIR/r3_q1.md、DIR/r3_q2.md、…として作成し、ルートの具体的な内容を含めてください(参照だけにしてはいけません。エンジンに渡されるのはクエリファイルと問題文だけです)。クエリに問題文をコピーしないでください。また、DIR/r3_verify.md をちょうど1つ作成してください。そこには、現在の証明草稿全体を DIR/proof.md からシェルの cat コマンドでそのままコピーして収め、段階ごとの検証を依頼してください。すべての不等式、置き換え、引用結果、「したがって」の各箇所について、記述どおりに本当に導けるかを確認し、誤りや穴を重大度の高い順にすべて挙げ、主張全体が証明されているかを明示的に述べるよう求めてください。 どのルートが実際に成立するかを簡単な計算で確認できる場合は、python3 を使用してください。DIR/notes.md を書き直してください。作成したファイルの一覧を含め、100語未満で返信してください。

FINALIZE BRIEF

ステップ:最終化。ファイル:問題は DIR/problem.md、実行中のメモは DIR/notes.md、コミットウェーブに提出された証明の草稿は DIR/proof.md、コミットウェーブの結果は DIR/r3_q*.answer.md、検証クエリの報告は DIR/r3_verify.answer.md です(存在するファイルは DIR/index.md に記載されています。存在しない場合は草稿をもとに最終化してください。インデックスで「partial」と記されたクエリには、代わりに DIR/r3_q{k}.partial.md または DIR/r3_verify.partial.md があります。これは打ち切られたエンジンの未完了のメモで、未検証です。その中の証明は結論ではなく確認すべき手がかりであり、打ち切られた検証報告に記載された未解決箇所も確認する価値がありますが、最終判定がないことからは何も判断できません。各完了ファイルの末尾にある「=== END OF ANSWER … ===」行は管理上のものです)。主張台帳は DIR/ledger.md です。これらをすべて読んでください。

あなたは難しい数学の問題に対する、構造化された並列アプローチを実行しています。コミットウェーブから結果が返ってきました。あなたの役割はプロトコルの最終ステップとして、最良のコミット結果(または、どのコミットクエリもそれを上回らなかった場合は草稿)をもとに最終的な proof.md をまとめることです。反復してください。検証クエリが欠落を見つけた場合は、手元の資料から修正できるものを修正してください。依拠する具体的な計算上の主張はすべて python3 を使って確認してください。最終文書では、残る欠落について正直に記述してください。明確に欠落と示すほうが、取り繕うよりも価値があります。最終文書には問題の答えを示し、完全な論証を記し、その後に「Status」という短い節を設けて、主張が完全に証明されているかどうかを明記し、残る欠落を列挙してください。また、「Other routes」という短い節も設け、記録に値するその他の内容を記述してください{PARTIALS_FIN}。最新の [GOAL] 行が PROVED でない場合、または PROVED でも 2 行の [AUDIT] による認証を受けておらず、その証明が検証報告と修正を経ても成立しない場合に、台帳に有効な別の主張に対する PROVED [GOAL] 行があるなら(目標は達成後に引き上げられています。複数ある場合は最も新しいものを選びます)、その証明済みの目標を文書の定理として述べて証明する主張とし、より弱い結果として提示してはいけません。引き上げられた目標については、その後に未達の目標として報告し、主張の欠落として扱ってはいけません。「Status」節には、どの主張が主張本体であるかと、引き上げられた目標に達していないことを明記してください。proof.md は、このディレクトリ内の他のファイルを開けない査読者が単独で読むものです。proof.md では実行ファイル(r*_q*、extra_q*、*.answer.md、検証報告、メモ、スクリプト)を決して引用せず、依拠する論証をすべて proof.md に完全に書いてください。必要であれば作業ファイルから書き直してください。まず受け取った草稿を DIR/judge/finalize_previous_proof.md として保存し、その後、最終版の DIR/proof.md を作成してください。DIR/notes.md も書き直してください。200 語未満で返信してください。最初の行は厳密に「MAIN CLAIM: PROVED」または「MAIN CLAIM: NOT PROVED」で始めてください(上記で定義した proof.md の主張本体について、「Status」節で示す判定です。ここで PROVED とは、その主たる結果、つまりその主張の証明または反証が完全であることを意味します)。同じ行にダッシュを続け、その主張本体を 1 つの節で記してください。その後に「Status」の段落を続けてください。

{PARTIALS_FIN} は SHORT 末尾では空であり、R < ESC_ROUND の場合も空です。FULL 末尾で R ≥ ESC_ROUND の場合は、次のとおりです(先頭の空白も含みます)。「 (概略のみ記された、または追究されなかった経路。ただし、目標に関係するすべての証明済みの還元、再定式化、特殊ケースは本文に含め、最も一般的なものから順に完全に記述すること)」

コメント