siege

math-proof: siege

方法

该技能在最多 MAX_ROUNDS 轮内处理一个问题。每一轮，一名评判者会写若干自包含的问题，在第 ESC_ROUND 轮之前最多为 WAVE 个。以下步骤称它们为查询。每个问题交给一个全新的 worker，它只能看到该问题和问题陈述。评判者阅读答案，重写当前摘要，并添加到一份声明台账中，声明标记为 PROVED、REFUTED 或 OPEN。其中一条声明是目标，在第 1 轮设定；评判者可以在后续轮次设定新目标，尤其是在目标被证明后，可以将其提升为更重要的陈述（被证明的目标随后作为后备结果留在台账中，如果两波未能使提升后的目标更接近，评判者就回到该后备结果；当目标被提升时，你要告知用户，并将已证明的结果复制到 DIR/result-so-far.md）。当某个答案包含对目标的完整书面证明或反证时，另外两个 worker 会逐行核对那段确切的文本。一旦两者都通过，评判者就得出结论或提升目标。在第 MIN_ROUNDS 轮之前，这是得出结论的唯一方式。从第 ESC_ROUND 轮起，如果手中没有完整的证明或反证，一轮可以最多保留 WAVE_DEEP 个问题，交给更高投入的 worker。除最多两个外，其余问题都针对证明中仍然缺失的那一个陈述。轮次结束后，评判者写出一份自包含的 proof.md，一名 worker 检查它，评判者再定稿。除非本次运行结束时所依据的目标在轮次期间既被证明又被检查了两次，否则在定稿前还会有额外的修订遍和最后一波完整证明尝试。proof.md 有一个 Status 部分，直白说明哪些被证明、哪些没有被证明。这一部分只是摘要：你自己不做任何数学工作，你严格按以下步骤执行，为每个评判者步骤和每个 worker 启动一个全新的子 Agent。

你是本协议的 ORCHESTRATOR。你自己不做数学，也不评判数学：评判由全新的 math-proof-judge 子 Agent 完成，每个步骤一个；推理由全新的 math-proof-worker 或 math-proof-worker-deep 子 Agent 完成，每个查询一个（用哪一个由轮次编号决定——见 Rules）。你的工作是严格运行以下步骤，保持文件有序，根据记账脚本打印出的那一个机械判定采取行动，绝不因为问题看起来简单或困难就跳过、合并或重排步骤。不要自己阅读 worker 的答案文件（用 test -s 查看文件是否存在；是否完成由记账脚本而非你决定）；不要在任何评判者会读到的地方用自己的话总结数学——传递文件，而不是转述。全程无人值守地工作到结束：没有人可以回答问题。 参数。 调用消息内容为：$ARGUMENTS 它给出问题，并可选地给出设置。按如下方式解读。位于其开头、形如 NAME=value 的记号， 其中 NAME 是由两个或更多大写字母和下划线组成的词，value 是整数（对于 DIR 则是路径，若含空格则加引号）， 是设置（以下七项，或 DIR，即运行目录；任何其他此类 NAME 都是错误，见“设置”）；将这些记号移除。若剩余内容是单行，且整体来看—— 去掉首尾空白和一对包围的引号，反斜杠转义的空格按空格读取 ——是某个现有文件的路径（该路径可能含空格；用 Read 或 Glob 检查，而不要用 shell），则该文件就是 问题文件；若不存在这样的文件，且剩余内容只能是一个文件路径——单行并以 .md、 .txt 或 .tex 结尾，或单个记号（去掉引号后不含空格）含 "/" 或 ""——用一句话告诉用户， 在你查找的绝对路径下（给出该路径）不存在文件，并说明问题可以改为在命令后以完整文本给出， 然后停止；否则剩余的全部内容，直到消息结尾，就是问题陈述，逐字照录——包括数学内容、换行等一切（MAX_ROUNDS=8 是设置； "n=3"、"N=pq"、"AB=AC" 和 "f(x)=…" 是数学内容）。运行目录 DIR 默认为当前目录下的 ./math-proof-run；下文一律使用 DIR 的绝对路径。若消息中既无可读的问题 文件，也无任何问题文本，用一两句话说明——并给岀用法，/math-proof:siege [NAME=value …] <问题陈述，或存放问题陈述的文件路径>，以及：已停止的运行可通过在同一目录中再次给出其 原始行来恢复——然后停止。 设置（除非调用消息按名称覆盖它们，否则使用这些值）：ESC_ROUND = 4（升级 轮：从第 ESC_ROUND 轮起，若循环仍在运行，波次上限提高，每个 worker 都是 math-proof-worker-deep，且计划简报带有其升级条款）；WAVE = 4，即在 ESC_ROUND 之前的各轮中每轮最多查询 4 次，而 WAVE_DEEP = 10，即从第 ESC_ROUND 轮起每轮最多查询 10 次；MAX_ROUNDS = 14； MIN_ROUNDS = 4（裁判可从第 MIN_ROUNDS 轮起自由作出结论，更早则只有在 账本中有经审计的链时才可以——由脚本决定）；REFINE_STEPS = 2；MAX_COMMIT = 9（二者均适用于完整 证明尾部；若某次运行的最终目标在轮次期间即已获认证，则采用短尾部——见“证明尾部”）。调用消息可按 名称覆盖这七项中的任意一项，方式是使用形如 NAME=value 的记号（例如 MAX_ROUNDS=8 WAVE_DEEP=6），将其放在问题之前、 调用消息的开头：按给定值使用，并将此处此类记号（NAME 是由两个或更多大写字母和下划线组成的词，value 是整数） 中 NAME 既不是这七项之一也不是 DIR 的情况视为错误——用一句话告诉用户， NAME 不是 /math-proof:siege 的设置，可接受的名称是 DIR、ESC_ROUND、WAVE、WAVE_DEEP、 MAX_ROUNDS、MIN_ROUNDS、REFINE_STEPS 和 MAX_COMMIT，并且如果该记号本身是问题的一部分， 则可将问题以文件路径形式给出——并在创建任何内容之前停止。（开头记号若其 左侧是单个字母或并非全为大写，或其右侧不是整数，以及 问题陈述内部更深处的任何"="，都是数学内容，而非设置。） 下文凡提到某项设置，均指生效值。 记账脚本是本 skill 自身文件夹中的 scripts/ledger.py：python3 ${CLAUDE_SKILL_DIR}/scripts/ledger.py （下文称为 SCRIPT）。若该占位符未被填充—— /scripts 之前的路径不存在——则使用 ${CLAUDE_PLUGIN_ROOT}/skills/siege/scripts/ledger.py，若该占位符也未被填充，则在 ~/.claude 下 Glob 查找 **/skills/siege/scripts/ledger.py 并使用其绝对路径（若匹配到多个，取最新的）；无论 哪种情况，若脚本路径含空格，在命令中将其加引号。在 Setup 之前，不带其他参数运行一次 SCRIPT： 它应打印一行以 "usage:" 开头的内容。若 Python 运行了，但提示无法打开该 脚本文件，则是路径错误，而非 Python 的问题：按上述回退方式重新解析并再次运行，若 找不到任何 ledger.py，则告诉用户该插件的文件不在预期位置（从 /plugin 重新安装 math-proof）并停止。若 shell 提示找不到 python3，或返回任何不是 usage 行的其他内容（在 Windows 上，回复称 Python“未找到”且可从 Store 安装，即属 此种情况），则此后在 SCRIPT 中用 python 代替 python3 并再次运行；若仍然失败， 用一两句话告诉用户 /math-proof:siege 无法运行其记账脚本——引用该命令 和 shell 的回复——说明它需要在 PATH 上以 python3 或 python 提供 Python 3.7 或更高版本， 并且修复后再次给出同一行即可运行；然后停止。

设置

1. 如果 DIR/state.md 已经存在，这是一次恢复：检查现有的 DIR/problem.md 是否与你收到的问题相同 （比较文本，忽略空白和行尾差异；如果是文件，用 cmp）—— 如果不同，用一句话说明 DIR 中保存的是针对另一个问题的一次运行，且 DIR=<另一个 目录> 可选择一个新的目录，然后停止；如果相同且 state.md 记录着 "phase: finished"，则该次运行 已完成：说明 DIR/proof.md 在哪里（以及 DIR/result-so-far.md，如果存在），说明 DIR=<另一个 目录> 会启动一次全新的运行，然后停止；否则完整 Read DIR/problem.md，读取 state.md 并从它记录的阶段 恢复，而不是从头开始，绝不重做输出文件已存在的步骤，也 绝不重写 DIR/problem.md（如果调用消息给出的设置与 state.md 中记录的不同， 在与你的下一次工具调用同一条消息中包含一行，说明以记录的设置为准——这是通知，不是停止）。如果记录的阶段是一个 wave，从该 wave 的 查询词干上运行 SCRIPT answers 开始（参见 Rules 下的 wave 规则），并且只为脚本未报告 已回答的查询启动 worker，每个部分完成的查询都带上其 {EARLIER} 段落；该次启动算作该 wave 的第一次，因此其一次 重跑仍然适用。一个已经回答但其索引行缺失的查询会得到该行 "{Q} | answered | (finished before this session resumed)"；一个已经有索引行的查询不会再得到 第二行——其新状态会作为 " | re-run: status | abstract" 追加到该行。 否则创建 DIR 和 DIR/judge/（mkdir -p）并将问题放到 DIR/problem.md：如果 它是作为文件传来的，用 cp 逐字节将该文件复制到那里；如果它是作为调用消息中的文本传来的， 就将该文本原样 Write 到 DIR/problem.md（不添加、删除或改写任何内容）。然后，作为你的下一个 动作，完整 Read DIR/problem.md——你要将其文本粘贴到每个 judge brief 和每个 worker 提示词中（参见 Rules）。
2. 写入 DIR/state.md（protocol math-proof siege，七个设置及其生效值——标记任何被调用 消息覆盖的设置——，"phase: round 1 plan, attempt 1"）。在恢复时，以 state.md 中记录的值为准。

轮次循环 — 对于 r = 1, 2, …, MAX_ROUNDS

(a) 规划。 启动一个 math-proof-judge，其提示词为下面的 PLAN BRIEF，其中填入 {r}、DIR 以及各轮次相关的 槽位（并且在重试时，在顶部加上脚本给出的更正段落）。各槽位： {CAP} 是本轮查询数量的上限 — 当 r < ESC_ROUND 时为 WAVE 设置，当 r ≥ ESC_ROUND 时为 WAVE_DEEP 设置 — 并且同一个数字也要放进 (b) 的检查命令中；{MAX_ROUNDS} 是 MAX_ROUNDS 设置，写成数字；{HORIZON}、{CONCLUDE_RULE}、{ESC_SUMMARY} 和 {ESC_WAVE} 是 brief 之后针对本 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} = 本轮的 cap，WAVE 或 WAVE_DEEP，与 (a) 中完全一致 — 在第 ESC_ROUND 轮或之后传入 WAVE 会悄悄地将一部分 wave 搁置）。它会自行对本轮的 账本行进行编号并追加到 DIR/ledger.md，并打印恰好一行判定；根据其第一个词采取行动（如果它改为打印以 ERROR: 开头的一行，则说明命令本身格式有误 — DIR 在前，作为绝对路径，然后是四个数字；请 更正命令并再次运行，这不算一次规划尝试）：

• WAVE n FLOOR f … — 将 DIR/round{r}_summary.md 复制覆盖到 DIR/summary.md，记下 f（本 wave 中最少可以返回已作答或部分作答状态的查询数，见 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: " 之后的文本作为 brief 新增的第一段；然后将尝试编号加一再次运行 (b)。
• TAIL: <reason> — 规划步骤失败了三次；将该原因记录到 state.md，如果 DIR/round{r}_summary.md 存在且非空，则将其复制覆盖到 DIR/summary.md，并离开循环进入证明 收尾 — 除非不存在 DIR/summary.md，且完全不存在任何 .answer.md 或 .partial.md 文件（没有什么可据以起草）：那么改为停止并报告。 目标变更通知：在 WAVE 或 CONCLUDE 判定时，如果该判定所接受的规划启动回复（即 最新一次尝试）中有一句以 "Goal change:" 开头的句子（judge 在本轮替换、提升或回到某个目标 — brief 的第 2 项）， 则将该句子加引号作为一行文本，放在你下一次工具调用的同一条消息中给用户 （这是通知，不是问题：仅有文本的消息会结束你的回合 — 不要停下或等待）， 并将同一行记录到 state.md。如果该句子以 "Goal change: raised" 开头，则先将其 指明为持有较早目标证明的文件（对每个文件执行 test -s）复制到 DIR/result-so-far.md — 一个文件：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） 的最后一个 "—" 之后的定位符中取出 <stem>，并使用 DIR/<stem>.answer.md，或者 如果只存在 DIR/<stem>.partial.md 则使用它；先对每个文件执行 test -s，如果都不存在，则跳过复制并在你的行中说明。 该文件是给在此处停止运行的用户用的；之后没有任何内容会读取它，而 proof.md 仍是 本轮的交付物。（对于固定其主张的问题，提升永远不会发生 — 没有什么可提升到的 — 因此 该文件永远不会被写入；替换仍会宣布。） 在任何情况下都要在 state.md 中记录其 wave 实际运行过的最后一轮的编号 R（(c)–(d) 完成后 R = r；当 循环在第 r 轮其 wave 之前离开时，R = r−1；如果从未运行过 wave，则 R = 0）。DRAFT BRIEF 需要它。 (c) Wave。 运行本轮查询文件的 wave（见 Rules：每个文件一个 worker — 在 ESC_ROUND 之前的轮次中为 math-proof-worker， 从第 ESC_ROUND 轮起为 math-proof-worker-deep —，全部放在一条消息中，脚本的 answers 判定、索引行、对 未作答查询的一次重新运行，然后是 FLOOR 停止规则）。 (d) 筛选（不启动）。 没有单独的筛选步骤：下一轮的规划 judge 会自行筛选本 wave 的 答案（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）中 标题目标已被确认，且由两个独立的 verify 查询认证，收尾部分为 SHORT：(e) 起草，(f) 无 refine 步骤，无 select 步骤——按 (g) 中所述的 shell 拼接方式自行构建 DIR/r3_verify.md， 不写任何 r3_q 文件——，(h) 一个仅包含 DIR/r3_verify.md 的提交波次，(i) 收尾。如果它打印 其他任何内容（通常是 REJECT: …），则收尾部分为 FULL：步骤 (e)–(i) 完全按下文所写执行——但以 ERROR: 开头的一行 意味着 gate 命令本身格式有误（DIR 在前，作为绝对路径）：纠正它并再次运行 后再做判断。在 state.md 中记录 "tail: short" 或 "tail: full" 以及 gate 的那一行。有两个回退机制守护 SHORT 收尾。如果其仅 verify 波次在唯一一次重跑后结束时没有 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 报告）；此回退最多适用一次，第二遍无论 (i) 的回复第一行说什么，都将 (i) 执行到结束。 (e) 起草。 一个 math-proof-judge，携带 DRAFT BRIEF（{R} 来自 state.md；{PARTIALS} 是 当收尾为 FULL 且 R ≥ ESC_ROUND 时 DRAFT BRIEF 之后给出的文本，否则为空——SHORT 收尾，或 R < ESC_ROUND；如果 R = 0 则将 brief 的 "final round's results" 子句替换为 "(no wave completed before the rounds ended — work from the summary and ledger)"）→ DIR/proof.md。额外查询规则适用（见 Rules；那次重启如果发生，属于本步骤）。如果 步骤结束后 DIR/proof.md 不存在，再次启动起草裁判，并添加第一段 "DIR/proof.md was not written; write it now from the material named below."；如果它仍不 存在，停止并报告。 (f) Refine，在 FULL 收尾中执行 REFINE_STEPS 次（步骤名按顺序为 refine_2、refine_3、……，共 REFINE_STEPS 个），在 SHORT 收尾中完全不执行：每次一个 math-proof-judge，携带 REFINE BRIEF（额外查询规则适用，每步一次）。 (g) Select。 一个 math-proof-judge，携带 SELECT BRIEF → 至多 MAX_COMMIT 个文件 DIR/r3_q{k}.md 以及恰好一个 DIR/r3_verify.md。如果之后 DIR/r3_verify.md 不存在，用 shell 创建它，不重新输入 任何内容，作为以下内容的拼接：行 "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) 提交波次。 将每个 DIR/r3_q{k}.md（SHORT 收尾中没有）加上 DIR/r3_verify.md 作为一个 波次运行（此波次无 screen 步骤）。 (i) 收尾。 一个 math-proof-judge，携带 FINALIZE BRIEF（{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 裁判一次，携带 FINALIZE BRIEF，并在其前添加 第一段 "DIR/proof.md still refers to run files (grep found: {the matches, at most ten, comma-separated}). 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 在哪里， 运行了多少轮以及循环为何结束（脚本的裁决行），运行了多少个 worker 查询，多少 被回答以及多少以 partial 结束，目标是否曾被替换或提高（一行，来自 state.md；如果 DIR/result-so-far.md 存在，说明它保存了 worker 所写的较早结果，仅按所记录的目标变更行进行了检查， 且 proof.md 及其 Status 部分取代它），以及裁判在其 finalize 回复中的 Status 段落，引用。 不要自己复述或评估数学内容。

全程适用的规则

• 每一个评审步骤和每一个 worker 都是一次新的 subagent 启动（Agent 工具），并显式设置 subagent_type；绝不能省略。这些 sub-agent 随本插件一起发布，你的 agent 列表通常以插件作用域名称显示它们 — math-proof:math-proof-judge、math-proof:math-proof-worker、math-proof:math-proof-worker-deep。逐个席位决定使用哪个名称：对于这三个中的每一个，如果你的 agent 列表提供了裸名称（math-proof-judge、math-proof-worker、math-proof-worker-deep），就用裸名称，否则用作用域名称；两种形式混用没有问题（用户或项目的 agents 目录中一个裸名称副本，就是用户修改该席位设置的方式，并且它本就应当胜出）。如果这三个中有任何一个在两种名称下都没有列出，告诉用户 math-proof 插件的 sub-agent 不在本会话的 agent 列表中 — 打开 /plugin 检查 math-proof 是否已安装并启用，重启 Claude Code，并再次给出同样的 /math-proof:siege 命令行 — 然后在第 1 轮之前停止。将每个席位使用的名称记录到 state.md 中。评审步骤使用 math-proof-judge。Worker — 轮次波次及其重跑 — 在 ESC_ROUND 之前的轮次使用 math-proof-worker，在 ESC_ROUND 及之后的每一轮使用 math-proof-worker-deep；证明尾部的 worker（额外查询波次、提交波次、r3_verify）如果在 ESC_ROUND 或之后的轮次（state.md 中 R ≥ ESC_ROUND）运行了波次，则使用 math-proof-worker-deep，否则使用 math-proof-worker。这个选择纯粹依据轮次编号，绝不依据你自己对尝试进展的看法。绝不重用、恢复或向更早的 subagent 发送消息。不要向 Agent 工具传递 model：评审和 worker 都运行在本会话的模型上。在一条消息中启动整个波次，使 worker 并行运行；绝不在后台运行 subagent。
• 在下面的每一份 brief 和 worker 提示词中，DIR 代表运行目录的绝对路径，其他 {花括号} 槽位代表所命名的值；替换它们，并逐字发送其余文本。不要向任何 brief 或提示词添加鼓励、提示、关于问题的看法、截止时间或结果摘要。
• 每一次 math-proof-judge 启动都要加上一项固定内容：在 brief 之后，追加一个空行、这一行“问题陈述（供参考 — DIR/problem.md 是权威文本；凡本副本有差异或看起来乱码之处，以该文件为准）：”，然后是 DIR/problem.md 的完整内容，逐字节照抄（你在设置期间已读取它）。它是参考材料，因此评审的第一条请求就已包含该问题；它不改变 brief 中的任何指令，而且 brief 中“评审不得将问题陈述复制到查询文件”的规则依然成立；每个 brief 都提到的 DIR/problem.md 仍然是权威文本。（Worker 提示词以下面给出的固定形式携带同样的文本。）务必精确粘贴：逐字复制你从 DIR/problem.md 读到的文本，绝不要凭记忆，也绝不要重新输入。
• 你自己绝不编写或编辑查询文件、答案文件（已完成的或部分的）、摘要、账本文件、notes.md 或 proof.md。你唯一编写的文件是 state.md、index.md、问题副本、回退 r3_verify.md 和 result-so-far.md（后两者仅通过复制或拼接）；除此之外，你只在某一步骤如此规定时复制或移动文件（cp/mv：summary.md，以及证明尾部中的 r3_verify.first 重命名）。除了确认答案文件存在（test -s）之外，你不读取它们；其中哪些已完成由记账脚本（下文 SCRIPT answers）判定，绝不由你判定。
• Worker 提示词始终完全如下，其中 {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." 结束行是用来区分已完成的答案与 worker 在中途被切断的答案（由于用量限制、错误或回合上限）的标志；记账脚本会检查它，你绝不检查。
• 运行一个查询文件波次意味着：为该波次使用的类型（math-proof-worker 或 math-proof-worker-deep，见第一条规则）的每个文件启动一个 worker，全部在一条消息中。当所有 worker 都返回后 — 绝不能更早：仍在运行的 worker 仍在写它的文件 — 运行 SCRIPT answers DIR {Q1} {Q2} …，参数为该波次查询文件的主名，作为独立命令运行，并在编写任何索引行或启动任何东西之前阅读它打印的内容。它在你不阅读任何内容的情况下判定哪些答案文件已完成，并为每个查询打印一行 — "{Q}: answered"（DIR/{Q}.answer.md 以该查询的结束行结尾：其 worker 完成了它）、"{Q}: partial"（某个 worker 写了些内容但从未完成；脚本已将该未完成文件移动到 DIR/{Q}.partial.md，因此 .answer.md 文件始终意味着已完成的答案）或 "{Q}: no answer" — 然后是一行 "TOTAL (n queries): …"，带有三个计数（如果它改为打印一行 ERROR，可以安全地更正命令 — 先是 DIR，然后是诸如 round2_q1 的主名 — 并再次运行）。 向 DIR/index.md 追加每个查询一行：" {Q} | answered | "、"{Q} | partial | " 或 "{Q} | no answer | "，与脚本所说一致，后接 worker 给你的回复的前 300 个字符（其摘要 — 不是答案文件的内容），将换行替换为空格，使该条目保持在一行。然后，如果 — 且仅当 — 该波次的某个查询未得到回答，则为每个这样的查询重新启动一个新的 worker（一次，全部在一条消息中；对已回答的查询不启动任何东西；partial 查询的提示词携带 {EARLIER} 段落，从而把未完成文件交给新 worker），当它们全部返回后，再次以该波次的所有主名运行 SCRIPT answers（已回答的查询不受影响），并向每个重跑查询的现有索引行追加（用 Edit 工具；该查询不新增第二行） " | re-run: answered | "、" | re-run: partial | " 或 " | re-run: no answer | " 按它现在报告的结果，后接新 worker 回复的前 300 个字符，如前所述（一个被切断两次的查询保持 partial；脚本在两个未完成文件中保留较长的作为 DIR/{Q}.partial.md，另一个放在它旁边作为 DIR/{Q}.partial.prev.md）。 因此一条索引行读作 "{Q} | status | abstract"，有时后接 " | re-run: status | abstract"，而重跑的状态（若有）即为生效状态；plan、draft、refine 和 finalize 的 brief 会告诉评审 partial 文件是什么。绝不在 worker 返回到为其记账的 answers 运行之间为某个查询启动 worker。注意该波次最后一次 answers 运行的 TOTAL 行 — 即对该波次所有主名运行的那次，因此其计数 n 等于该波次的大小：下面的 FLOOR 规则和 state.md 都使用它。
• 本会话期间没有任何用户会回答你：绝不要结束回合去询问如何继续，绝不要等待确认，也绝不因为出了差错就提前停止 — 按这些规则决定并持续前进，直到协议完成或下面某条规则说要停止。返回错误、被中断的结果或空回复的 subagent 会被记录到 index.md / state.md 中，协议继续；丢失一个 worker 是正常的；返回错误或被中断的评审步骤会立即重新启动一次。如果同一个评审步骤连续两次失败（出错，或没有写出它的任何文件），就停止并报告当前进展。如果在某一轮的波次经过其唯一一次重跑后结束，最后一次 TOTAL 行上的 answered + partial 小于脚本在其 WAVE 判定中打印的 FLOOR 数字（筛选判定不计入此限），就停止并报告：存在系统性问题，继续下去只会把评审步骤浪费在无谓的事情上 — 告诉用户最可能的原因是用量限制或中断切断了 worker，本次运行的文件完好无损，并且在该原因清除后，在同一目录再次给出同样的 /math-proof:siege 命令行即可恢复运行。（如果那条 TOTAL 行的 n 小于该波次，说明你只对部分主名运行了 answers — 先对全部主名运行它。）额外查询波次和提交波次没有下限。
• 额外查询：当 draft 或 refine brief 允许时，评审最多可写出 3 个名为 DIR/extra_q{k}.md 的文件，使用下一个未使用的编号 k；整个运行的预算是 10（一旦 DIR/extra_q10.md 存在，就不得再写 — brief 中已说明）。当评审的回复说它写出了额外查询文件时，确认它们存在，将其作为一个波次运行（它们的答案落在 DIR/extra_q{k}.answer.md，或被切断两次的落在 DIR/extra_q{k}.partial.md — 索引会说明是哪种），然后带着这段新增的首段重新启动同一步骤一次："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." 重新启动的步骤产生的第二批额外文件留在磁盘上不予回答。
• 在每个步骤之后重写 DIR/state.md：协议、设置、当前阶段、尝试计数器，以及一份逐步增长的每步一行日志；每一轮的 plan 行还记录传给 check 命令的波次上限，每个波次的行还记录启动的 worker 类型和最后的 TOTAL 行（例如 "cap 10, math-proof-worker-deep ×9, answered 8, partial 1, no answer 0"）。如果本次对话被压缩，它是你唯一的记忆；如果你不确定自己身处何处，重新阅读 state.md 和 ${CLAUDE_SKILL_DIR}/SKILL.md。

计划简报（第 {r} 轮，最多 {MAX_ROUNDS} 轮；{CAP}、{HORIZON}、{CONCLUDE_RULE}、{ESC_SUMMARY} 和 {ESC_WAVE} 取决于 r，见 (a) 及下文）

步骤：计划第 {r} 轮，最多 {MAX_ROUNDS} 轮。{HORIZON} 文件：问题是 DIR/problem.md；你的运行笔记是 DIR/notes.md；上一轮的运行摘要为 DIR/summary.md（第 1 轮中不存在）；声明 账本是 DIR/ledger.md（在记录任何内容之前不存在或为空）；上一轮的结果是 文件 DIR/round{r-1}_q*.answer.md，其在 DIR/index.md 中的行给出的状态为 "answered"（每行内容为 "query | status | abstract"，有时后接 "| re-run: status | abstract"，此时以重跑的 状态为准；第 1 轮中无此类文件），另有 DIR/extra_q*.answer.md（若存在）。状态为 "partial" 的查询 对应的则是文件 DIR/round{r-1}_q{k}.partial.md：这是一个中途被截断的引擎的笔记。也要阅读它，以获取线索以及 构建新查询的素材，但其中没有任何内容被确立——它可以引出一条 OPEN 行或一个查询，绝不能单独引出一条 PROVED 行（一个例外：如果它 包含对 [GOAL] 声明或对更早提出且仍受下述审计规则覆盖的某个目标的完整书面证明或反驳，则该证明算作"在手"， 用于审计规则，就如同该文件已 完成一样——你还要写下审计和结论规则所要求的已确立的 [GOAL] 行，以该 查询的词干（例如 round3_q2）作为其定位符——随后由验证查询来裁定）。 （每个已完成的结果文件末尾都有一行簿记内容 "=== END OF ANSWER … ==="：它不是数学的 一部分；在你拼接或引用任何内容时都要将其排除。）先阅读问题、你的笔记、摘要、账本和 索引，然后阅读上一轮的结果文件——每个文件一次，完整阅读。

0. 先筛选（第 2 轮及以后）。在你阅读上一轮的结果文件时，检查每个文件是否真正针对其查询——不是拒绝作答、空文件或近乎空白的文件、离题文字，或针对 不同问题的工作。写入 DIR/judge/screen_r{r-1}.md，对该轮每个查询一行，内容恰好为 "round{r-1}_q{k}: OK" 或 "round{r-1}_q{k}: DEGENERATE: 一行理由"（对于状态为 no answer 的查询， 写 "DEGENERATE: no answer"；partial 查询的 .partial.md 按与已完成文件相同的标准筛选—— 未完成本身不算退化），并在下文所有内容中忽略你标记为 DEGENERATE 的每个文件。 这是筛选，不是评分：一个错误、薄弱或不完整的答案仍然是 OK。

你在指导对一道困难数学问题的结构化多轮尝试。每一轮，你编写查询，这些查询被独立发送给一个具有极大思考预算的深度推理引擎； 结果以文件形式返回，你在编写下一轮之前将其中确立的内容汇入运行摘要。这是第 {r} 轮，最多 {MAX_ROUNDS} 轮。{HORIZON} {CONCLUDE_RULE}

按顺序做以下三件事。

1. 更新运行摘要。从头将其重写为 DIR/round{r}_summary.md：它取代 先前的摘要，并且是后续轮次（以及最终证明汇编）对先前所发生一切的唯一记忆，因此要结转所有仍然相关的内容。记录：已经确立的内容，引用展示它的结果 文件（例如 round2_q3）；有前景的部分进展；死胡同，以及每条为何是死胡同；以及 当前状态与目标之间存在的未解缺口。要诚实——过度声称的摘要会毒害 之后的每一轮。保持在 6000 字以内。然后决定下一步瞄准哪里：在摘要末尾写一节，指明下一轮应集中 于哪里——锐化最强的部分结果、弥合最承重的未解缺口、验证该尝试现在所依赖的某内容，或 放弃一条死线以换用全新视角。早期轮次通常探索（多样的独立重构和方法）；后期轮次 通常利用（聚焦尝试、关键步骤的验证）。每轮的选择由你决定。{ESC_SUMMARY}

2. 更新声明账本。除摘要外，本次运行还维护一个带编号的声明账本，每条标记为 PROVED、REFUTED 或 OPEN。与摘要不同，账本从不重写：你现在写入的行逐字 追加（编号已为你添加），现有条目只有通过追加一条明确命名其编号的 RETRACT 行才失去效力。写入 DIR/round{r}_ledger_block.md，其中只包含本轮的新行， 每行一条，形式为 "PROVED: 一句话声明 — 定位符"、"REFUTED: 一句话声明 — 定位符"、 "OPEN: 一句话声明 — 定位符"（定位符 = 结果文件词干，例如 round2_q3），或 "RETRACT 4: 一句话理由，说明条目 4 为何不再成立"。为 本轮确立或开启的每条承重声明追加一行；对于状态发生变化的任何声明写一条新行（该声明的最新 行取代较旧的行），并对现已确知错误的内容写一条 RETRACT 行。每行保持一句话：整个账本会逐字带入之后的每一轮以及最终证明汇编—— 它是本次尝试中唯一无法被折叠掉的记忆。在陈述首要目标的行中，在状态词后紧接着标记 [GOAL] （"PROVED: [GOAL] …"、"OPEN: [GOAL] …"），并用 [AUDIT] 标记一条 PROVED 行，记录某个单独的验证查询检查了一条完整书面证明链（命名该查询的 定位符，并引用它所认证的条目为 "entry N" 或 "#N"）。行出现时即打标签。在第 1 轮中恰好写一条 [GOAL] 行。如果问题固定了 待确立的声明，则该声明——所提出的完整声明，所有部分——即为目标；如果任务是 开放式的（改进、扩展或强化给定工作；找到关于某事物的重大结果），现在就选择 目标——一个精确陈述，即你判断本次尝试能够确立的最重大结果——并将其 记录为 [GOAL] 行，在确立之前保持 OPEN。(i) 状态行。仅当同一 声明的状态发生变化时（OPEN → PROVED 或 REFUTED，或在验证查询发现缺口时回到 OPEN——那时还要 RETRACT 该 PROVED 行）才为该声明再写一条 [GOAL] 行——并且要在其结果文件首次包含完整书面证明的那一轮就写，这样你在同一步中编写的验证查询认证的就是一个在其答案返回时已经编号的行 ——或按下文 (iv) 回到它；绝不只是为了改写它，因为只有最新的 [GOAL] 行算数， 而 [AUDIT] 行必须按编号引用它所认证的 [GOAL] 条目，即目标自那时起未变时的那条最新条目（你块中的行从 DIR/ledger.md 的最后一条条目开始编号，按文件顺序）。(ii) 更改目标。目标并非固定：在之后的任何计划步骤你都可以通过写一条新的 OPEN [GOAL] 行来设定新目标，从那时起它即为 目标（这并非在第 1 轮就定低目标的理由：第 1 轮目标的选定完全如上）； 在本简报全文中，"the [GOAL] line" 和 "the [GOAL] claim" 意指当前生效的最新 [GOAL] 行及其 声明。有两个理由设定新目标。替换目标（RETRACT 旧的 [GOAL] 行——如果它曾是 PROVED 且该证明成立，则将它所证明的内容作为一条普通的不带标签的 PROVED 行重新录入——然后写入新的 目标）如果它被证明为假、不适定或已知，并且如果你发现它比问题本身提出的声明更窄或 不同——那么所提出的声明就是新目标（这是替换，而非提升，即使较窄的目标已 被 PROVED：对于固定其声明的问题，本次运行的裁定是关于该声明的）；对于你在第 1 轮在开放式任务上自行选择的目标，被反驳意味着替换它并继续（对于你提升到的目标，见 (iii)），而 一条 REFUTED [GOAL] 行仅当问题本身提出该声明时才结束本次运行。或者提升目标：一旦当前目标被 PROVED，如果现在看起来在剩余轮次内可及一个更重大的结果——一个 更强的陈述，或所证明内容的更一般情形——则将该新陈述写为一条 OPEN [GOAL] 行 （定位符 roundN_plan，N 为本轮编号），其标准与第 1 轮的选择相同（一个 精确陈述，你判断本次尝试能够确立的，而不是据你所知为假、不适定或已知的陈述）。提升始终是一条 OPEN 行：绝不要把比结果文件实际证明的更强的声明写成 PROVED [GOAL] 行。当问题本身提出该声明且它已按所提出的样子被证明时，就没有什么可提升的：作结论。(iii) 提升会留下什么。当你提升时，不要撤回被证明的目标或其 [AUDIT] 行：它们作为普通条目继续有效，如果提升后的目标未达成，该结果正是最终文档所呈现的内容。如果某个验证查询在你提升离开的目标的证明中发现缺口，则 RETRACT 其 PROVED [GOAL] 行——绝不要让一条其证明未通过检查的 PROVED [GOAL] 行继续有效——并在 (ii) 下重新决定哪个陈述是目标（要回到较早的那个，将它写为最新的 OPEN [GOAL] 行，并将该波次瞄准该缺口）。一条被 REFUTED 的提升目标不是本次运行的裁定，其反驳不需要验证查询（下述审计规则针对的是本次运行可能据以作结论的目标）：将其记录为一条 "REFUTED: [GOAL] …" 行，命名反驳文件，然后在其下重新陈述你已证明的目标，如 (iv) 所述，并据此作结论。提升是判断，不是义务：如果没有明显更重大的东西看来可及，就根据本简报前文给出的作结论规则对已证明的目标作结论；如果瞄准提升目标的前两个波次（提升轮自身的波次是第一个）没有让它更接近——没有它的证明，也没有通往它的新路线——那么在下一个计划步骤回到已经证明的目标并作结论。回退优先于摘要的链条和进展规则以及下文的升级规则，后者仅在某个停滞的陈述仍为目标时指挥一个波次瞄准它：一个回退的步骤除了审计规则对它返回的目标仍要求的验证查询外不编写任何查询（一个审计波次，然后作结论）。除回到已经证明的目标外，不要因为某目标难以证明就将它换成更弱的目标：朝着未达成目标所确立的内容，由证明撰写步骤按其原样呈现。你不采纳为目标的更强或更远的结果，保留为普通的 PROVED/OPEN 行，属于证明的"其他路线"部分。(iv) 回退。要回到先前已证明的目标（所提升的陈述未产生结果），在本轮块中将其重新陈述为一条 "PROVED: [GOAL] …" 行，引用其较早条目为 "entry N" 或 "#N"，放在本块所持的任何其他 [GOAL] 行之后，使其成为最新的（行按文件顺序编号），并在其下将其认证重新陈述为 [AUDIT] 行，每行如前命名其验证查询的定位符，并以相同形式引用新行的编号（计算一下：如果 DIR/ledger.md 结束于条目 23，而重新陈述的目标是你块中的第二行，则它是条目 25）——当重新陈述的目标行引用了较早条目时，一条此类行就足够，否则要两条，来自不同的查询；然后根据作结论规则作结论。如果没有声明被确立、开启、更改或撤回，则将文件留空。

3. 编写下一轮的查询——或作结论。当且仅当手中的材料完全确立了目标时，写入 DIR/round{r}_DONE.md，包含一行 指明材料在哪里确立它，并且不写任何查询（如果你在这一步提升目标，则改为为其编写一个波次——绝不要在同一步中既提升又写 DIR/round{r}_DONE.md）。否则写入 1 到 {CAP} 个查询文件 DIR/round{r}_q1.md、DIR/round{r}_q2.md、… （连续编号）瞄准你选择的目标。当 [GOAL] 行处于 OPEN 时，并行查询既廉价又独立，因此 尽量用掉大部分预算；让它们成为对目标真正不同的尝试，而不是同一个尝试的改写。一旦 [GOAL] 声明的完整书面证明（或反驳）已 在手，波次就缩小：编写下述审计规则所要求的验证查询加上至多 2 个其他查询，瞄准 最终证明文档将需要的内容（一个推论的完整撰写、一个仅被引用的引理的证明、一个独立的第二证明）。如果相反你在这 一步提升目标（第 2 项），波次不缩小：已证明链条的验证查询仍然发出——当它们的认证在之后 一轮返回时，将它们记录为 [AUDIT] 行，命名其定位符并按编号引用它们所认证的目标的 PROVED 条目，即使目标此后已经 转移——而波次的其余部分，直至上限，是为新的 OPEN [GOAL] 行编写的。当本简报带有下文 升级规则时，波次的该部分遵循它，以所提升的陈述作为手中没有其证明的 [GOAL] 声明：先回去为所提升的陈述给摘要写它的"The chain and the missing statement"一节（摘要规则 (iii)；如果还没有任何东西 归约它，则所提升的陈述本身就是那个缺失的陈述，其 OPEN [GOAL] 行充当 其账本条目），然后在升级规则下编写波次的该部分。每个查询必须自包含：推理引擎只看到该查询文件后跟完整问题陈述——没有摘要、没有账本、没有其他结果、没有其他轮次——因此要内联包含该查询所依托的任何先前结果或部分 论证（用 shell 从答案文件中拼接长段落，而不是重打它们）。不要将问题陈述本身复制到任何查询中。 瞄准规则（每轮适用）。在你编写的查询中，至少一半（向上取整）必须尝试本次运行自己标记过的 未决问题：结果文件中命名的未决问题、账本中的 OPEN 声明，以及你摘要中的未解缺口。通过让每个此类查询的第一行恰为 "kind: attempt" 来标记它，并在其中命名它所尝试的具体未决问题。尝试查询试图确立其问题——证明它、反驳它，或将其归约到严格更容易的东西——而不是 综述它、重新推导其周围的已知内容，或润色文档。某个问题"已确立：未决"（或目标超出当前技术水平）的裁定不是最终的，后续轮次不得将其当作已确立而继承： 重新开启它，并让尝试查询直接瞄准它。 审计规则（每轮适用）。每当手中的某个结果文件给出 [GOAL] 声明——或你在本步或更早提升离开的目标（不是你提升到的目标的反驳：第 2 项 (iii)）——的完整书面证明（或反驳），且尚无两个验证查询认证它时，本轮查询中至少与仍缺失数量相同（两个或一个）的查询 必须是对该书面链的独立验证查询——如果多个结果文件各给出一个完整证明， 挑选最完整的一个，并将两个验证查询都针对同一链条发出。每个都逐字携带完整论证—— 用 shell 从答案文件组装查询文件（cat、sed；从部分文件组装时，遵循上文文件列表所给的 例外），不要重打或转述它——并 请求逐步检查每一个推理，最后明确裁定该链条是否严格按所陈述的样子证明了 该声明；它们算作尝试查询（第一行 "kind: attempt"，命名它们审计的 [GOAL] 条目）；两个认证即满足门槛——只有当第三个检查了前两个未检查的内容时才再加一个。当这样的认证返回 为正面时，将其记录为一条 PROVED [AUDIT] 行，命名其定位符并按编号引用它所认证的 [GOAL] 条目（该目标的那条已确立行，即使目标此后已被 提升）；当账本随后满足条件（见上文）时，作结论。{ESC_WAVE} 检索规则。运行摘要是压缩，可能丢弃或颠倒某个结果实际所说的内容。 每当你依赖或反驳先前结果时——在摘要重写、账本行、你的目标 选择，或作结论的决定中——先阅读该结果的答案文件，并从它实际所说的内容出发，而不是从摘要对它的转述出发。

最后重写 DIR/notes.md，并用 150 字以内回复：已作结论与否、查询文件数以及其中有多少是尝试查询，并用一句话说明目标。如果你本轮替换、提升或回到了一个 目标（第 2 项），再加一句，不计入 150 字，以 "Goal change:" 开头—— 三者中的哪一个，目标过去是什么、现在是什么（各用短语），以及已经成立的已证明结果（若有），带其账本条目编号以及迄今有多少验证查询认证了它；对于 提升，还要按完整路径命名持有该结果完整证明的答案文件（形式为："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 时，恰好是：“你可以在本轮得出结论，早于第 {MIN_ROUNDS} 轮， 只要主张账本中标题目标已定论 —— 即一条标记为 [GOAL] 的 PROVED 或 REFUTED 行（“PROVED: [GOAL] …”）—— 并且至少有两条标记为 [AUDIT] 的 PROVED 行。每条 [AUDIT] 行都是某个单独 verify 查询返回的 认证，该查询检查了完整的书面证明链（不是草图或提纲）；它必须写明该查询的定位符（例如 round3_q2）并引用 [GOAL] 行，或它所引用的某行，以账本 id 写作“entry 12”或“#12”—— 至少有一条 [AUDIT] 行引用 [GOAL] 行本身。当账本符合条件时，在这一步于两件事之间作出决定： 得出结论，或提升目标（下文第 2 项说明何时以及如何）并为提升后的目标组织一轮 wave。不要仅仅为了达到 第 {MIN_ROUNDS} 轮或为了润色而继续运行 wave —— 后续的 证明撰写步骤会完成润色。在行出现时为其打标记。如果账本尚不符合条件， 则组织一轮 wave（下文的审计规则说明它何时必须包含 verify 查询）。” —— 而当 r ≥ MIN_ROUNDS 时，它恰好是：“从本轮起，只要手头材料 完全确立了 [GOAL] 主张，你就可以随时得出结论 —— 除非手头已有完整书面证明而认证它的 verify 查询 尚不足两个，此时下文的审计规则仍适用于本轮（一轮审计 wave，然后得出结论）—— 并且当这样的证明已在手头时， 本轮的账本块必须已经携带已定论的 [GOAL] 行，以账本的普通形式 写作‘PROVED: [GOAL] …’（或‘REFUTED: [GOAL] …’），状态词与标签之间不得有任何内容 —— 它尚未 获得认证这一点无需自己的标记，[AUDIT] 行记录认证 ——，就在组织其 verify 查询的同一步中。一旦 [GOAL] 主张得到确立，你要么得出结论（在其审计 wave 之后，即审计规则适用之处），要么提升目标（下文第 2 项；提升无需等待审计），但绝不在同一步中两者兼为：提升目标的步骤不写 DONE 文件，因为提升后的目标由一轮 wave 定论，而非由得出结论定论。如果你在较早轮次中提升了目标，而 提升后的陈述尚未产生结果，你可以就已被证明的目标得出结论，按第 2 项 (iv) 所述将其重新陈述为最新的 [GOAL] 行。在最后一轮，这样做，而不是让轮次简单地耗尽。”

{HORIZON} 在 r ≤ MAX_ROUNDS−2 时为空；当 r = MAX_ROUNDS−1 时，它恰好是：“所以本轮之后最多还能再运行 一轮。”而当 r = MAX_ROUNDS 时恰好是：“所以这是最后一轮：它的查询返回什么，就直接进入证明撰写步骤，之后没有可据以行动的 进一步轮次。”（注意开头的空格。 简报中的 {MAX_ROUNDS} 是写作数字的 MAX_ROUNDS 设置，每一轮都是。） {ESC_SUMMARY} 在 r < ESC_ROUND 时为空；当 r ≥ ESC_ROUND 时，它正好是（包含开头的空格）： " 从本轮起，再有四条规则支配摘要；因为规则 (iii) 要求你自己做数学，先在写下由结转材料与 (i)–(ii) 组成的摘要文件，再去完成 (iii)，然后扩展它——一条只用于思考的消息可能被截断，而未被写下的内容就会丢失。(i) 既有结果：保留一个以此命名的部分，列出每一条已证（PROVED）的账本行，只要它是关于该问题整体（所有参数）的定理、是对 [GOAL] 主张的精确重述或归约到一个命名的更简单或经典陈述、或是某个自然特例的完整解——每条都带上其定位符——即使它本身无法完成目标；永远不要从这个部分删除条目（改为标记为 '不在当前主线上'），因为如果目标未达成，最终文档就是围绕这些条目构建的。(ii) 死路：一条路线只有在存在精确陈述被反驳（REFUTED）且反驳它的结果文件被记录为恰好那种形式时，才算死路。一个结果文件报告某个障碍、在某个拟设或某个候选内部搜索失败，或某条路线只到达目标的一部分，关闭的是那个候选，而不是那条路线：把这类路线列在未解决的缺口下，标记为 '搁置，未被反驳'，可重新攻击。(iii) 链条与缺失陈述。首先判断是否已经掌握对 [GOAL] 主张的完整书面证明或反驳。一个结果文件，如果恰好按所述证明了上一轮的缺失陈述，且该链条不需要任何进一步的东西，它就是一个完整的书面证明：在这种情况下，把 [GOAL] 行记为 PROVED（或对反证记为 REFUTED）写入本轮的账本块，按编号引用链条所用的条目，并指明新证明的定位符，然后编写审计规则的验证查询，使其携带整个链条——所引用条目的论证与新证明，各自从其答案文件拼接，按上一轮摘要所述的链条推导精确连接。如果已经掌握完整的书面证明或反驳，无论以那种方式还是任何其他方式，跳过 (iii) 的剩余部分和全部 (iv)。否则，摘要中包含一个标题恰好为 '链条与缺失陈述' 的部分，每轮重写，含四个带标签的部分。链条：[GOAL] 主张（或其否定，当所追求的是一条反证时——那么下面读作 '缺失陈述的证明'）从已经 PROVED 的结果——按账本编号引用，只写陈述——连同恰好一个尚未证明的进一步陈述推导出来的过程；把推导一步一步写出来，使得持有被引用条目和那一个陈述的证明的读者就能得到完整证明。如果材料尚未把目标归约到单个陈述，则把主线下一步所需的最强中间主张取为缺失陈述，并在链条中说明在它之后还剩下什么。缺失陈述：那一个陈述，完整而自足地写出——每一个量词、每一个对象都定义，并且它可能用到的每一个问题假设都与它一起陈述（一个被剥离了它实际需要的假设的陈述会变为假，而对其的反驳随后会毁掉一条可靠的路线）。它可以带有自己的假设——对某些对象或参数范围的一部分的限制——只有链条在引用 PROVED 条目时表明那些假设之外的一切都已解决时才可如此；一个其证明仍会使问题所允许的某些对象悬而未决的陈述，是一个特例，而不是缺失陈述。在能完成链条的诸陈述中，优先选择最简单、最具体的。首次陈述它以及每当其措辞变化时，把它作为一条 OPEN 行记入账本（定位符写 roundN_plan，N 为本轮编号）——然后还要 RETRACT 它所替换的措辞的 OPEN 行——以便后续轮次和查询可以引用它。它为何应成立：你自己的草图，最多十五行，说明你为何相信它以及它可能通过何种论证被证明——自己动手做这些数学：如果你能看到某种可能给出它的候选机制，不论何种，都精确陈述出来；你的一个随后由引擎证明或反驳的猜想，是这一步产生的最有用的东西之一。迄今尝试：已经在陈述或其较早措辞上花费的每个查询一行——定位符、所采取的方法、它产出什么（特例的证明、等价重述、障碍、什么也没有）；同一任务的相同副本共用一行；如此列出的方法算作已尝试。(iv) 进展检验。开启目标部分时说明过去两轮是否在链条上产生进展，只把以下计入进展：缺失陈述的证明；[GOAL] 主张的证明；一个对假设所允许的每个对象都成立并缩短链条的新 PROVED 结果；或用严格更简单的陈述替换缺失陈述（更简单，而不是更窄），链条重新推导。当缺失陈述的难点仍然未决时解决对象的又一部分——以致该陈述只是变窄——或对它做等价重述，记录在 (i) 下，但不算这种意义上的进展。如果没有进展，写 '主线停滞——无普遍进展'，用一行说明你的草图或分解与上一轮有何不同，不要以开启另一个特例或转向其他路线求宽度作为回应：本波次（除非第 2 项 (iii) 现在让你回到一个已经证明的目标并作结）按下面的收尾规则对准缺失陈述本身，必须改变的是你 (iii) 中自己的草图——针对同一陈述的不同机制，或对链条作不同分解从而得到不同的缺失陈述。如果某个结果文件恰好按所述反驳了缺失陈述，不要仅仅通过排除反例的类别来挽救它（除非有 PROVED 条目已经解决那个类别，且链条如此说明）：要么陈述一个修正后的缺失陈述并为它完整地重新推导链条，要么按 (ii) 把该行记为死路，并构建下一条最有希望路线的链条。从本轮起，'验证' 作为目标只意味着审计规则的目标审计和收尾规则项 (c) 所允许的那一个链条检查。" 当 r < ESC_ROUND 时，{ESC_WAVE} 为空；当 r ≥ ESC_ROUND 时，它恰好是（包含前导空格；{CAP} 按其他位置的替换方式替换）：

" Escalation rule（本轮以及之后的每一轮，只要尚未获得 [GOAL] 命题的完整书面证明或反驳——一旦获得，包括 summary rule (iii) 所描述的、已证明的缺失陈述补全链条的情形，则上面所述的 audit rule 和缩小的 wave 接管，下面的 (a)–(c) 随即被忽略）。回答本轮的引擎拥有比开局轮次大得多的思考预算，且该 wave 最多可容纳 {CAP} 个查询：用掉其中大部分，并将它们花在你链条中缺失的陈述上，完整表述——不要花在综述上，也不要为广度而广度。(a) 每个查询都要发起攻击：它尝试缺失的陈述、[GOAL] 命题本身，或一个其答案能够解决或严格缩减其中之一的提问（仅对部分对象解决不算缩减）。不要将查询花在撰写、打磨、重新推导或验证那些不能补全 [GOAL] 链条的结果上——轮次之后的证明撰写步骤会以它们自己的查询预算来完成这些——因此一轮中唯一的 verify 查询是 audit rule 的查询（对已证明后又升高的目标进行认证的 verify 查询算作 audit rule 的查询）以及 (c) 所允许的那一个链条检查项。不要花查询要求引擎从文献中回忆或重构证明，无论是 [GOAL] 命题的还是其他任何东西的：引擎没有可查阅的文库，这样的任务没有给它们任何可推理的东西（在攻击中调用已知定理是另一回事，没问题）。（仅在最后两轮——本简报开头的 'Step: plan round …' 行届时会明确说明，措辞为 "one further round" 或 "the final round"；如果两者都没有，这就不是那两轮之一——最多两个查询可以改为验证或完整撰写最终文档将呈现的现有结果。）(b) Closing rule。 写一个任务文件，要求给出你链条中恰好那个缺失陈述的完整证明——或者给出它的一个明确反例——并且包含：该陈述，逐字如 summary 所述；它可能依赖的每一个先前结果，连同其来自答案文件的证明完整拼接进来（cat, sed——绝不转述）；链条从它推导出 [GOAL] 的过程，以便引擎看到该陈述是为了什么，并在该推导本身有缺陷时能够指出；你关于它为何应成立的草图，作为引擎可自由丢弃的建议提供；以及明确的一句话：仅对该陈述所涵盖的部分情形——其对象的某个子类或其参数的某个子区间——的证明并不回答该问题，尽管如果只找到这些也应报告。将其保存为本轮的查询文件 q1（上述文件中的第一个），并逐字节复制（cp）到 q2 和 q3：三个引擎独立尝试同一陈述——对同一个表述良好的陈述进行独立尝试，在这里比分别对三个陈述各进行一次尝试更有价值。这些完全相同的副本是有意为之（上面关于对同一尝试改述的禁令不适用于它们），且三者都是 attempt 查询（首行 'kind: attempt'，将缺失的陈述命名为它们所尝试的开放问题）。(c) 其余查询——用掉上限的大部分——同样指向缺失的陈述，每个都自包含（除下文另有说明外，携带相同的拼接内容），且每个要么是 closing 任务的又一逐字节副本（允许：这是又一次独立尝试），要么与它真正不同：由 'Tried so far' 下未出现的指定方法发起的攻击（在任务中命名它；引擎可以偏离它，只要说明理由）；或从它返回的部分结果继续推进的所列方法，并将该结果拼接进来；或你自己草图中最难的单步，切出来并作为一个自包含命题提出；或某个结果文件针对该陈述提出的那一个障碍，作为待克服之事提出，或精炼为反例。在第一轮中会提出一个缺失陈述，且每当其措辞改变时再次如此，这些查询之一改为完全按其所述尝试反驳它——通过明确构造，或通过从它推导出已知为假的东西。当同一个缺失陈述已在之前两轮中被攻击时，这些查询之一只被给予该陈述和所引条目的陈述（无证明，无草图），并被要求先自行推导出该陈述将补全 [GOAL]，然后以所列尝试都未用过的第一步攻击它——若引擎发现该推导不成立，或该陈述不可信，就说明，这是需按 summary rule (iv) 采取行动的结果。该 wave 中至多两个查询可以另作他用：指向主线并非源自的路线（按 summary rule (ii) 搁置，而非反驳），或——其中至多一个——检查链条所依赖的、尚无单独查询检查过的一个已证明步骤。所有这些查询都是 attempt 查询（首行 '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 都在那里供按名称查阅（一个 DIR/…_q{k}.partial.md 文件，若索引将其查询标记为 partial，就是一个被截断的引擎未完成且未经验证的 笔记：仅是线索，其中没有任何内容得到确立；而每个已完成文件末尾的 "=== END OF ANSWER … ===" 行 是记账，不是数学）。 先阅读问题、笔记、总结、台账和最终轮的结果。

你正在指导对一道困难数学问题的结构化多轮尝试。各轮已经结束。 你现在的任务：编写 DIR/proof.md，包含通向目标的最强路线——即这次尝试找到的最完整的论证——并完整写出其论证，{PARTIALS} 外加一段简短说明，记录每一条其他值得记录的路线， 以及一份对任何仍然存在的缺口的诚实陈述——一个清楚标记的缺口比一个被粉饰的缺口更有价值。如果最新的 [GOAL] 行不是 PROVED——或者是 PROVED 但未经两条 [AUDIT] 行认证，且其书面证明无法通过你自己的检查——并且台账中有效持有一条针对不同主张的 PROVED [GOAL] 行（一个先被达成随后又被提升的目标；若有多个，取最近的），那么那个已证明的目标就是 proof.md 的主要主张。将其陈述为文档的定理，并根据台账为它指定的结果文件完整写出其论证（若台账指定的文件是一个 .partial.md 文件，则从承载它的验证查询文件及其答案认证它的地方取文本）；它不属于次要结果。被提升的目标 排在它之后，作为一条被尝试过的陈述，连同朝它已确立的一切，而状态部分说明哪个是哪个。每当具体计算能确认或推翻一个步骤时，就使用 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 时，它恰好是（包含开头的空格）：" and — because the newest [GOAL] line is not certified — also written out in full with their proofs, in the body (after the theorem of an earlier proved goal, when the sentence below about a raised goal applies) and ahead of the statement of what remains open: every PROVED result in the ledger or summary that settles a natural special case, gives an exact reformulation or reduction of the goal (state it as a theorem: 'the claim holds for all … provided …'), or identifies the goal or its open core with a named known statement, the most general first — for a goal the attempt did not settle, a referee judges it by the reductions and partial results it actually establishes, so these are the document, not side notes;"

REFINE BRIEF（步骤名 {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 检查你依赖的每一个具体计算论断。如果一次有针对性的深度推理查询就能解决一个承重缺口，你可以把它写成下一个未使用的 DIR/extra_q{k}.md（本步骤最多 3 个；一旦 DIR/extra_q10.md 存在就不能再写），自包含——引擎只会看到该文件后接题目陈述，所以请内联包含它所依据的一切，不要将题目复制进去——并在回复中说明你这样做了。然后完整重写 DIR/proof.md，先将收到的草稿保存为 DIR/judge/{S}_previous_proof.md。对你仍然存在的缺口要诚实——一个清楚标明的缺口比一个被粉饰的缺口更有价值。重写 DIR/notes.md。回复不超过 150 词。

SELECT BRIEF

步骤：为提交波选择路线。文件：题目是 DIR/problem.md；你的运行笔记是 DIR/notes.md；证明草稿是 DIR/proof.md；最终一轮的结果（以及你需要的任何更早的结果文件），见 DIR/index.md（其中标记为“partial”的查询只有未验证的笔记，位于 DIR/…_q{k}.partial.md，来自一个中途被中断的引擎）；论断台账 DIR/ledger.md。

你正在对一道困难数学题进行结构化的并行尝试；你已有一份证明草稿和全部探索结果。你的任务是协议的提交步骤：任何具有具体路线（一条指名引理链、一个具体构造）通向目标的成果，都要在完整思考预算下获得一次提交查询：“路线：[该路线]。写出完整的严格证明。” 另外还要有一次验证查询，逐步检查草稿证明的论证。（如果某个目标已被证明而后来提升的目标未被证明，草稿的主要论断就是那个已被证明的目标；通向提升目标的具体路线仍可提交。） 最多选择 {MAX_COMMIT} 条值得提交的路线（更少也可以——只有具备具体内容的路线才值得）。对每条路线，将查询写为 DIR/r3_q1.md、DIR/r3_q2.md、……，并在其中包含该路线的实际内容（而不是对它的引用——引擎除了查询文件后接题目陈述以外什么都看不到）。不要将题目陈述复制到任何查询中。还要写出恰好一个 DIR/r3_verify.md，其中包含完整的当前证明草稿（用 shell——cat——从 DIR/proof.md 完整复制，而非重新键入），并要求逐步检查：对每一个不等式、交换、引用结果和“由此可得”，它是否真的如所写那样成立；按严重程度列出每一个错误或缺口，并明确说明主要论断是否已被证明。 如果快速计算能确定哪些路线是真实的，就用 python3。重写 DIR/notes.md。回复不超过 100 词，并列出所写的文件。

收尾简报

步骤：收尾。文件：题目是 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 但未经两条 [AUDIT] 行认证，且其书面证明未能经受验证报告和你 的修复——而台账中持有针对另一个论断的有效 PROVED [GOAL] 行（该目标是在达成之后才被提升的； 若有多个，取最近的），那么主论断就是那个已证明的目标，作为文档的定理陈述并证明，而不是 作为次等结果呈现。被提升的目标在其后作为尝试报告，而不是作为主论断的缺口，且 Status 小节 直白说明哪个论断是主论断，以及被提升的目标未曾达成。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”开头（这是你的 Status 小节对按上述定义之 proof.md 主论断的判定；此处的 PROVED 意味着文档的主要结果——对该 论断的证明或反驳——是完整的），然后在同一行接一个破折号和该主论断的一句话表述，然后是 该 Status 段落。

{PARTIALS_FIN} 在 SHORT 尾部以及每当 R < ESC_ROUND 时为空；在 R ≥ ESC_ROUND 的 FULL 尾部中， 它恰好是（包括前导空格）：“ (routes only sketched or not pursued — whereas every PROVED reduction, reformulation or special case that bears on the goal belongs in the body, written out in full, the most general first)”