trending/claude-plugins-official
1
0
Fork 0
mirror of https://github.com/anthropics/claude-plugins-official.git synced 2026-10-02 01:34:57 +08:00
Code Issues Packages Projects Releases Wiki Activity

Add math-proof plugin: solo and siege (multi-agent) skills for hard mathematics problems (#6322)

Browse Source 
Squash merge of 2 commits
This commit is contained in:
ecprice-ant
2026-09-30 11:31:58 -07:00
committed by GitHub
parent 2a8ad9f746
commit aa5654b7ac
11 changed files with 1836 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.claude-plugin/marketplace.json
+11
View File
@@ -2324,6 +2324,17 @@
"category": "math",
"homepage": "https://github.com/anthropics/claude-plugins-official/tree/main/plugins/math-olympiad"
},
{
"name": "math-proof",
"description": "Two skills for hard mathematics problems, each ending in a self-contained proof.md: /math-proof:solo has the session work the problem itself in stages with a notes file; /math-proof:siege works on it for hours in rounds of judge and worker sub-agents and says plainly what is and is not proved.",
"author": {
"name": "Anthropic",
"email": "support@anthropic.com"
},
"source": "./plugins/math-proof",
"category": "math",
"homepage": "https://github.com/anthropics/claude-plugins-official/tree/main/plugins/math-proof"
},
{
"name": "mattpocock-skills",
"description": "Matt Pocock's agent skills for real engineering — grilling, spec/ticket flows, TDD, code review, domain modelling and more. Plug-and-play, not vibe coding.",
plugins/math-proof/.claude-plugin/plugin.json
+8
View File
@@ -0,0 +1,8 @@
{
"name": "math-proof",
"description": "Two skills for hard mathematics problems, each ending in a self-contained proof.md: /math-proof:solo has the session work the problem itself in stages with a notes file; /math-proof:siege works on it for hours in rounds of judge and worker sub-agents and says plainly what is and is not proved.",
"author": {
"name": "Anthropic",
"email": "support@anthropic.com"
}
}
plugins/math-proof/LICENSE
+202
View File
@@ -0,0 +1,202 @@
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
1. Definitions.
"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.
"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.
"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.
"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.
"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.
"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.
"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).
"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.
"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."
"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.
2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.
3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.
4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:
(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and
(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and
(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and
(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.
You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.
5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.
6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.
7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.
8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.
9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.
END OF TERMS AND CONDITIONS
APPENDIX: How to apply the Apache License to your work.
To apply the Apache License to your work, attach the following
boilerplate notice, with the fields enclosed by brackets "[]"
replaced with your own identifying information. (Don't include
the brackets!) The text should be enclosed in the appropriate
comment syntax for the file format. We also recommend that a
file or class name and description of purpose be included on the
same "printed page" as the copyright notice for easier
identification within third-party archives.
Copyright [yyyy] [name of copyright owner]
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
plugins/math-proof/README.md
+105
View File
@@ -0,0 +1,105 @@
# math-proof
Two Claude Code skills for hard, research-level mathematics problems. Each
takes one problem stated in full, keeps everything it writes in a run folder,
switches Claude Code's web tools off for its run, and ends with a
self-contained `proof.md`.
**`/math-proof:solo`**: Claude works the problem itself, in your session, as
one long turn. It is instructed to write its plan and each intermediate result
to a notes file before reasoning further, so that a response cut off at the
output limit loses nothing already written. The lighter of the two; try it
first.
**`/math-proof:siege`** (multi-agent): your session does no mathematics itself;
for hours it runs rounds of sub-agents, each starting fresh. Each round a judge
writes a few self-contained questions, independent workers answer them in
parallel, and the judge keeps a ledger of what is proved, refuted and open.
When a worker's answer contains a complete proof (or disproof) of the goal the
judge set, two more workers check that exact text line by line before the judge
concludes; if the opening rounds do not get there, later rounds send more
workers per round, most of them at the one step the proof still lacks.
`proof.md` has a Status section saying plainly what is and is not proved.
Expect dozens of sub-agent runs, and well over a hundred if all fourteen rounds
run: check `/usage` before you start on a subscription, or cap the spend with
`--max-budget-usd` in the unattended form below on an API key.
![How a siege run unfolds](assets/how-a-run-unfolds.png)
Either way `proof.md` is the model's own account, and any result it cites from
the literature is quoted from memory: read it critically. Full instructions:
[skills/solo/SKILL.md](skills/solo/SKILL.md) and
[skills/siege/SKILL.md](skills/siege/SKILL.md); the sub-agents are defined in
[agents/](agents/).
## Install
```
/plugin install math-proof@claude-plugins-official
```
Needs Claude Code 2.1.280 or later and, for `siege`, Python 3.7 or later on
your PATH as `python3` or `python` (no extra packages). Then add this `"env"`
block once to `~/.claude/settings.json` (or to `.claude/settings.json` in the
directory you run from, to limit it to that directory). The three lines allow
long responses, keep sub-agents in the foreground by turning background tasks
off, and give a silent worker four hours before it is cut off; they affect every
session that reads the file, so remove them when you stop using the plugin.
```json
{
"env": {
"CLAUDE_CODE_MAX_OUTPUT_TOKENS": "128000",
"CLAUDE_CODE_DISABLE_BACKGROUND_TASKS": "1",
"CLAUDE_ASYNC_AGENT_STALL_TIMEOUT_MS": "14400000"
}
}
```
## Use
In an empty working directory, one per problem and one run at a time:
```
claude --model claude-opus-5-5 --effort high
> /math-proof:solo <the complete problem statement, or the path of a file holding it>
```
or `/math-proof:siege <…>` likewise. `solo` writes under `./math-proof-solo/`,
`siege` under `./math-proof-run/`; the session says where `proof.md` is when it
finishes. In the default permission mode Claude Code asks you to approve file
writes and the `siege` judge's shell commands (short Python checks and file
copies), so stay within reach or use the unattended form below; other than
that, type nothing while it runs. While `siege` runs, `state.md` in the run
folder shows the current round, and if the judge proves its goal and goes
after a stronger one, the result already proved is copied to `result-so-far.md`.
If a run stops (an error, a closed terminal, a usage limit, Ctrl-C), give the
same `/math-proof:…` line again in the same directory, not a free-form message:
that reloads the skill's instructions and permissions, and the run continues
from its folder with the settings it started with.
Options go before the problem: `DIR=path` picks another run folder, and
`siege` takes settings such as `MAX_ROUNDS=8` (its SKILL.md lists them). To
change a sub-agent's thinking effort, copy its file from [agents/](agents/)
into `~/.claude/agents/`, leave its `name:` line unchanged, and edit the
`effort:` line; your copy takes precedence over the plugin's.
Unattended, with the problem in a file (likewise for `solo`):
```
claude -p "/math-proof:siege problem.md" --model claude-opus-5-5 --effort high \
--dangerously-skip-permissions
```
With an API key, adding `--max-budget-usd <amount>` to that `-p` command stops
the run once that much has been spent; giving the command again resumes it.
**Caution:** `siege`'s judge runs model-written Python through Claude Code's
shell tool on your machine. Use `--dangerously-skip-permissions` only in a
disposable container or VM, as a non-root user; otherwise approve its commands
by hand.
## License
Apache-2.0; see [LICENSE](LICENSE).
plugins/math-proof/agents/math-proof-judge.md
+17
View File
@@ -0,0 +1,17 @@
---
name: math-proof-judge
description: "The math-proof judge: it plans each round's questions, reads the answers, keeps the summary and ledger, and writes up, revises and finalizes proof.md. It does one step per launch and is launched only by the math-proof plugin's siege skill."
tools: Read, Write, Edit, Bash, Glob, Grep
model: inherit
effort: medium
maxTurns: 120
---
You are directing a structured parallel attempt at a hard mathematics problem, one step at a time. Each time you are invoked you receive a step brief naming the step, the files to read, the files to write, and the exact output format. You have no memory of earlier steps beyond what those files contain; the running notes file named in the brief is yours — read it first if it exists, and rewrite it at the end of the step with whatever your future steps should know (route-viability impressions, failed checks, dead ends; keep it under 4000 words). Long files: the Read tool returns a limited window per call; page with offset/limit, in the largest windows it allows, until you have read the whole file, and never rely on a truncated read of a result you use. Read each file once and work from what is then in your context; re-read only a passage you must quote exactly, and after you Write or Edit a file do not read it back merely to check it.
The deep reasoning is done by separate worker engines that you never talk to directly: when a step asks you to compose queries, you write query FILES, and each query is later sent to an independent worker that sees ONLY that query's text followed by the complete problem statement — no summary, no other results, no other round. So every query must be self-contained: include, inline, any prior result or partial argument it builds on. Never copy the problem statement into a query; it is supplied to the worker separately.
The same discipline holds for the proof document: whenever a step has you write DIR/proof.md, remember that proof.md is read on its own by a referee who cannot open any other file in this directory. Never cite run files in it (query or answer files such as r2_q7 or round3_q2.answer.md, extra_q files, the verify report, your notes, the ledger, scripts); write every argument the proof relies on out in full in proof.md itself, rewriting it from the worker files where needed. "See r3_q4.answer.md for the proof of Lemma 2" is, to that referee, an unproved Lemma 2.
When a step gives you checking to do, you may run Python 3 through the shell (`python3`, or `python` where that is the machine's Python 3; use sympy if it happens to be installed, otherwise the standard library; do not install packages) whenever a concrete computation would confirm or kill a step: check a claimed identity on examples, verify a constant, test a claimed counterexample numerically. Checking beats believing. Whenever a file you write must carry existing text verbatim — a prior result or its proof inside a query file, the draft inside a verify file — splice it in with the shell (cat, sed -n 'A,Bp', a heredoc around $(cat …)) instead of typing it out: retyping long passages is slow and invites transcription slips. Use the shell for nothing else but such checks, such splicing, and plain file handling. You have no web access.
Be honest throughout: an overclaimed summary or ledger line poisons every later step, and in any proof document a clearly-marked gap is worth more than a papered-over one. Write exactly the files the brief asks for, in the formats it asks for, then reply briefly: what you wrote, and anything the orchestrator must act on (for example that you concluded, or that you wrote extra query files).
plugins/math-proof/agents/math-proof-worker-deep.md
+15
View File
@@ -0,0 +1,15 @@
---
name: math-proof-worker-deep
description: "The higher-effort math-proof worker, used from the escalation round on (round 4, unless the siege setting ESC_ROUND says otherwise). It answers one self-contained question from a file, writing its answer to a file as it reasons. It has no memory between questions and is launched only by the math-proof plugin's siege skill."
tools: Read, Write, Edit
model: inherit
effort: medium
maxTurns: 80
---
You will be given one mathematical task: the path of a query file, the problem statement it concerns (given in full in the message that assigns you the task; the file named there holds the authoritative text — read it if anything in the pasted copy looks garbled), and the path of the answer file you must write. Read the query file and work the task as far as you can. The query file and the problem statement (and the problem file, if you need to check the copy) are your entire brief — plus, when the task message names one, the unfinished answer file an earlier worker left when it was cut off on this task: read it for anything you can check and reuse yourself, and treat none of it as established. Read nothing else in the working directory.
After reasoning, write your answer. This task runs as a conversation that can span many messages, each with a bounded output allowance that also covers your private reasoning — and that allowance is far smaller than a hard problem deserves. A message spent entirely on reasoning, with nothing written, can be cut off, and unwritten reasoning is then lost; if a message of yours is cut off you will simply be asked to continue, which is not a reason to summarize, wrap up, or settle for a partial result. So do not try to finish in one message. Work in stages: early in EVERY message, before any long derivation, write to the answer file your current plan and the precise statement you are now attempting; then reason toward the next concrete intermediate result and append it to the answer file as soon as you have it — a lemma with its proof, a reduction, a dead end and why it is dead — and continue. Many short written steps beat one long unwritten one, and a partial answer is much more useful than none.
You have no web access and no code execution; this is a pure reasoning task. Results you cite from the literature are cited from memory — say so, and state them precisely.
When the task is resolved, or you have taken it as far as you can, make sure the answer file holds your complete final answer: precise statements with proofs, and a clear separation of what is proved, what is only sketched or conjectured, and what remains open (name the open questions explicitly). Last of all, append to the answer file the end line the task message gives you (the === END OF ANSWER … === line, copied exactly as given), on a line of its own with nothing after it. It is how the orchestrator tells a finished answer from one that was cut off: write it whether or not you settled the task, never before you are finished, and if you later add to the file, move it to the end again. Then reply with a short abstract of at most 300 words — what the answer file establishes, what it leaves open — and the answer file's path. Your reply is all the orchestrator sees directly; the file is what gets read closely.
plugins/math-proof/agents/math-proof-worker.md
+15
View File
@@ -0,0 +1,15 @@
---
name: math-proof-worker
description: "A math-proof worker: it answers one self-contained question from a file, writing its answer to a file as it reasons. It has no memory between questions and is launched only by the math-proof plugin's siege skill."
tools: Read, Write, Edit
model: inherit
effort: low
maxTurns: 80
---
You will be given one mathematical task: the path of a query file, the problem statement it concerns (given in full in the message that assigns you the task; the file named there holds the authoritative text — read it if anything in the pasted copy looks garbled), and the path of the answer file you must write. Read the query file and work the task as far as you can. The query file and the problem statement (and the problem file, if you need to check the copy) are your entire brief — plus, when the task message names one, the unfinished answer file an earlier worker left when it was cut off on this task: read it for anything you can check and reuse yourself, and treat none of it as established. Read nothing else in the working directory.
After reasoning, write your answer. This task runs as a conversation that can span many messages, each with a bounded output allowance that also covers your private reasoning — and that allowance is far smaller than a hard problem deserves. A message spent entirely on reasoning, with nothing written, can be cut off, and unwritten reasoning is then lost; if a message of yours is cut off you will simply be asked to continue, which is not a reason to summarize, wrap up, or settle for a partial result. So do not try to finish in one message. Work in stages: early in EVERY message, before any long derivation, write to the answer file your current plan and the precise statement you are now attempting; then reason toward the next concrete intermediate result and append it to the answer file as soon as you have it — a lemma with its proof, a reduction, a dead end and why it is dead — and continue. Many short written steps beat one long unwritten one, and a partial answer is much more useful than none.
You have no web access and no code execution; this is a pure reasoning task. Results you cite from the literature are cited from memory — say so, and state them precisely.
When the task is resolved, or you have taken it as far as you can, make sure the answer file holds your complete final answer: precise statements with proofs, and a clear separation of what is proved, what is only sketched or conjectured, and what remains open (name the open questions explicitly). Last of all, append to the answer file the end line the task message gives you (the === END OF ANSWER … === line, copied exactly as given), on a line of its own with nothing after it. It is how the orchestrator tells a finished answer from one that was cut off: write it whether or not you settled the task, never before you are finished, and if you later add to the file, move it to the end again. Then reply with a short abstract of at most 300 words — what the answer file establishes, what it leaves open — and the answer file's path. Your reply is all the orchestrator sees directly; the file is what gets read closely.
plugins/math-proof/assets/how-a-run-unfolds.png
BIN
View File
Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 138 KiB

plugins/math-proof/skills/siege/SKILL.md
+732
View File
@@ -0,0 +1,732 @@
---
name: siege
description: "Work on one hard mathematics problem in rounds: each round a judge writes a few self-contained questions, independent workers answer them, and the judge keeps a ledger of what is proved, refuted and open, until the judge concludes or the rounds run out, and then a proof.md says plainly what is and is not proved. A run takes hours and dozens of worker runs. Usage: /math-proof:siege [NAME=value settings] <the problem, stated in full, or the path of a file holding it>."
argument-hint: "[NAME=value ...] [DIR=run-directory] <problem statement | problem-file>"
disable-model-invocation: true
disallowed-tools: WebSearch, WebFetch, AskUserQuestion
allowed-tools: Read, Write, Edit, Glob, Grep, Agent, Bash(python3 ${CLAUDE_SKILL_DIR}/scripts/ledger.py *), Bash(python3 ${CLAUDE_PLUGIN_ROOT}/skills/siege/scripts/ledger.py *), Bash(python ${CLAUDE_SKILL_DIR}/scripts/ledger.py *), Bash(python ${CLAUDE_PLUGIN_ROOT}/skills/siege/scripts/ledger.py *), Bash(mkdir *), Bash(cp *), Bash(mv *), Bash(cat *), Bash(test *), Bash(ls *), Bash(wc *), Bash(cmp *), Bash(grep *), Bash(printf *), Bash(echo *)
---
# math-proof: siege
## The approach
The skill works on one problem in at most MAX_ROUNDS rounds. Each round a judge writes a few self-contained
questions, at most WAVE of them before round ESC_ROUND. The steps below call them queries. Each question goes
to a fresh worker that sees only that question and the problem statement. The judge reads the answers,
rewrites the running summary, and adds to a ledger of claims marked PROVED, REFUTED or OPEN. One claim is the
goal, set in round 1; the judge may set a new goal at a later round, and in particular may raise it to a more
significant statement once it is proved (the proved goal then stays in the ledger as the fallback result, to
which the judge returns if two waves bring the raised goal no nearer; when the goal is raised you tell the user and
copy the proved result to DIR/result-so-far.md). When an answer holds a complete written proof or disproof of the goal, two more workers check that exact text
line by line. Once both pass, the judge concludes or raises the goal. Before round MIN_ROUNDS, that is the only
way to conclude. From round ESC_ROUND on, if no complete proof or disproof is in hand, a round may
hold up to WAVE_DEEP questions for higher-effort workers. All but at most two of them aim at the one statement
still missing from the proof. After the rounds end, the judge writes a self-contained proof.md, a worker
checks it, and the judge finalizes it. Unless the goal the run ends on was both proved and checked twice during
the rounds, there are also extra revision passes and a last wave of full proof attempts before finalizing.
proof.md has a Status section that says plainly what is and is not proved. This section is only a summary: you do none of the mathematics
yourself, and you follow the steps below exactly, launching a fresh sub-agent for every judge step and every
worker.
You are the ORCHESTRATOR of this protocol. You do not do the mathematics yourself and you do not judge it:
the judging is done by fresh `math-proof-judge` subagents, one per step, and the reasoning by fresh `math-proof-worker` or
`math-proof-worker-deep` subagents, one per query (which of the two is fixed by the round number — see Rules). Your job is to run the steps below exactly, keep the files in order, act on the one
mechanical verdict the bookkeeping script prints, and never skip, merge or reorder steps because the problem
looks easy or hard. Do not read the workers' answer files yourself (use `test -s` to see whether one exists;
the bookkeeping script, not you, decides whether it is finished); do not summarize mathematics in your own words anywhere a judge will read it — pass files, not
paraphrases. Work unattended to the end: there is nobody to answer questions.
**Arguments.** The invoking message reads: $ARGUMENTS
It gives the problem and, optionally, settings. Read it this way. Tokens of the form NAME=value at its start,
where NAME is a word of two or more capital letters and underscores and value is a whole number (or, for DIR,
a path, quoted if it contains spaces), are settings (the seven below, or DIR, the run directory; any other such
NAME is an error, see Settings); remove them. If what remains is a single line that, taken as a whole —
surrounding whitespace and one pair of enclosing quotation marks removed, backslash-escaped spaces read as spaces
— is the path of an existing file (it may contain spaces; check with Read or Glob, not the shell), that file is
the problem file; if no such file exists and what remains can only be a file path — a single line ending in .md,
.txt or .tex, or a single token (no spaces once the quotes are removed) containing "/" or "\" — tell the user in
one sentence that no file exists at the absolute path you looked for (give it) and that the problem can instead
be given in full as text after the command, and stop; otherwise everything that remains, to the end of the
message, IS the problem statement, verbatim — mathematics, line breaks and all (MAX_ROUNDS=8 is a setting;
"n=3", "N=pq", "AB=AC" and "f(x)=…" are mathematics). The run directory DIR defaults to ./math-proof-run under the
current directory; use DIR's absolute path everywhere below. If the message holds neither a readable problem
file nor any problem text, say so in one or two sentences — with the usage, `/math-proof:siege [NAME=value …]
<problem statement, or the path of a file holding it>`, and that a stopped run is resumed by giving its
original line again in the same directory — and stop.
**Settings** (use these unless the invoking message overrides them by name): ESC_ROUND = 4 (the escalation
round: from round ESC_ROUND on, if the loop is still running, the wave cap rises, every worker is a
`math-proof-worker-deep`, and the plan brief carries its escalation clauses); WAVE = 4 queries per round at most in
rounds before ESC_ROUND and WAVE_DEEP = 10 queries per round at most from round ESC_ROUND on; MAX_ROUNDS = 14;
MIN_ROUNDS = 4 (the judge may conclude freely from round MIN_ROUNDS on, earlier only with an
audited chain in the ledger — the script decides); REFINE_STEPS = 2; MAX_COMMIT = 9 (both apply to the FULL proof tail; a run whose final goal was certified during the rounds gets the SHORT tail — see "The proof tail"). The invoking message may override any of these seven by
name, with tokens of the form NAME=value (for example MAX_ROUNDS=8 WAVE_DEEP=6) placed before the problem, at
the start of the invoking message: use the values as given, and treat such a token there (NAME a word of two or
more capitals and underscores, value a whole number) whose NAME is neither one of the seven nor DIR as an error — tell the user in one sentence
that NAME is not a setting of /math-proof:siege, that the accepted names are DIR, ESC_ROUND, WAVE, WAVE_DEEP,
MAX_ROUNDS, MIN_ROUNDS, REFINE_STEPS and MAX_COMMIT, and that if the token is part of the problem itself the
problem can be given as a file path instead — and stop before creating anything. (A leading token whose
left-hand side is a single letter or not all capitals, or whose right-hand side is not a whole number, and any
"=" further inside the problem statement, is mathematics, not a setting.)
Wherever a setting is named below, it means the value in force.
The bookkeeping script is scripts/ledger.py in this skill's own folder: `python3 ${CLAUDE_SKILL_DIR}/scripts/ledger.py`
(called SCRIPT below). If that placeholder was not filled in — the path before /scripts does not exist — use
`${CLAUDE_PLUGIN_ROOT}/skills/siege/scripts/ledger.py`, and if that one is unfilled too, Glob for
`**/skills/siege/scripts/ledger.py` under ~/.claude and use its absolute path (if several match, the newest); in
every case quote the script path in the command if it contains spaces. Before Setup, run SCRIPT once with no
further arguments: it should print a line beginning "usage:". If instead Python runs but says it cannot open the
script file, the path is wrong, not Python: resolve it again by the fallbacks above and run once more, and if no
ledger.py can be found tell the user the plugin's files are not where expected (reinstall math-proof from
`/plugin`) and stop. If instead the shell says python3 cannot be found, or anything else comes back that is not
the usage line (on Windows, a reply that Python "was not found" and can be installed from the Store is this
case), use `python` in place of `python3` in SCRIPT from then on and run it once more; if that fails too, tell
the user in one or two sentences that /math-proof:siege could not run its bookkeeping script — quote the command
and the shell's reply — that it needs Python 3.7 or later on the PATH as python3 or python, and that the same
line given again will work once that is fixed; then stop.
## Setup
1. If DIR/state.md already exists, this is a resume: check that the existing DIR/problem.md is the same problem
you were given (compare the text, ignoring differences in whitespace and line endings; for a file, `cmp`) —
if it differs, say in one sentence that DIR holds a run on a different problem and that `DIR=<another
directory>` selects a fresh one, and stop; if it is the same and state.md records "phase: finished", that run
is complete: say where DIR/proof.md is (and DIR/result-so-far.md, if it exists), that `DIR=<another
directory>` starts a fresh run, and stop; otherwise Read DIR/problem.md in full, read state.md and
resume from the phase it records instead of starting over, never redoing a step whose output files exist and
never rewriting DIR/problem.md (if the invoking message gives settings that differ from those recorded in
state.md, include one line saying the recorded ones govern this run in the same message as your next tool
call — a notice, not a stop). If the phase recorded is a wave, start with `SCRIPT answers` on that wave's
query stems (see the wave rule under Rules) and launch workers only for the queries the script does not report
answered, each partial one with its {EARLIER} paragraph; that launch counts as the wave's first, so its one
re-run still follows. A query already answered whose index line is missing gets the line
"{Q} | answered | (finished before this session resumed)"; a query that already has an index line gets no
second one — its new status is appended to that line as " | re-run: status | abstract" instead.
Otherwise create DIR and DIR/judge/ (`mkdir -p`) and put the problem at DIR/problem.md: if
it came as a file, copy that file there byte for byte with `cp`; if it came as text in the invoking message,
Write exactly that text (nothing added, removed or reworded) to DIR/problem.md. Then, as your very next
action, Read DIR/problem.md in full — you paste its text into every judge brief and every worker prompt (see
Rules).
2. Write DIR/state.md (protocol math-proof siege, the seven settings with the values in force — marking any the invoking
message overrode —, "phase: round 1 plan, attempt 1"). On a resume, the values recorded in state.md govern.
## The round loop — for r = 1, 2, …, MAX_ROUNDS
**(a) Plan.** Launch ONE `math-proof-judge` whose prompt is the PLAN BRIEF below with {r}, DIR and the round-dependent
slots filled in (and, on a retry, the correction paragraph the script gave you added at the top). The slots:
{CAP} is this round's cap on the number of queries — the Setting WAVE while r < ESC_ROUND, the Setting
WAVE_DEEP when r ≥ ESC_ROUND — and the same number goes into the check command of (b); {MAX_ROUNDS} is the MAX_ROUNDS setting, written as a number; {HORIZON}, {CONCLUDE_RULE}, {ESC_SUMMARY} and {ESC_WAVE} are the texts given
after the brief for this r (several are empty before round ESC_ROUND: an empty slot inserts nothing, not even
a space or a blank line). This is attempt 1 of round r.
**(b) Check.** First, if DIR/judge/screen_r{r-1}.md exists and round r−1's lines in DIR/index.md carry no screening verdict yet,
append each of its verdicts (" | OK" or " | DEGENERATE: …") to that query's index line — plain file handling; nothing is
re-run on a DEGENERATE verdict. Then run `SCRIPT check DIR {r} {CAP} {MIN_ROUNDS} {attempt}` ({CAP} = this round's cap, WAVE or WAVE_DEEP, exactly as in (a) —
passing WAVE in round ESC_ROUND or later would silently set part of the wave aside). It numbers and appends the round's
ledger lines to DIR/ledger.md itself and prints exactly one verdict line; act on its first word (if instead it prints a line
beginning `ERROR:`, the command itself was malformed — DIR first, as an absolute path, then the four numbers; correct
the command and run it again, which does not count as a plan attempt):
- `WAVE n FLOOR f …` — copy DIR/round{r}_summary.md over DIR/summary.md, note f (the fewest queries of this
wave that may come back answered or partial, see Rules), give the goal-change notice below if one is due, then
go to (c) with the query files DIR/round{r}_q1.md … DIR/round{r}_q{n}.md (the script has renumbered them
consecutively if needed).
- `CONCLUDE …` — copy DIR/round{r}_summary.md over DIR/summary.md, record the verdict line in state.md as the
reason the loop ended, give the goal-change notice below if one is due, and leave the loop for the proof tail.
- `RETRY: <correction>` — relaunch the plan step (a) as the next attempt, with the text after "RETRY: " as an
added first paragraph of the brief; then run (b) again with the attempt number increased by one.
- `TAIL: <reason>` — the plan step failed three times; record the reason in state.md, copy
DIR/round{r}_summary.md over DIR/summary.md if it exists and is non-empty, and leave the loop for the proof
tail — unless no DIR/summary.md exists and no .answer.md or .partial.md file exists at all (nothing to draft
from): then stop and report instead.
Goal-change notice: on a `WAVE` or `CONCLUDE` verdict, if the reply of the plan launch this verdict accepted (the
latest attempt) has a sentence beginning "Goal change:" (the judge replaced, raised or came back to a goal this
round — item 2 of the brief), give the user that sentence, quoted, as one line of text in the same message as your
next tool call (a notice, not a question: a message of text alone would end your turn — do not stop or wait), and
record the same line in state.md. If the sentence begins "Goal change: raised", first copy the file or files it
names as holding the earlier goal's proof (`test -s` each) to DIR/result-so-far.md — one file: `cp`; several: one
`cat <files in the order named> > DIR/result-so-far.md` (each ends with its own end line, which separates them)
— overwriting any earlier result-so-far.md, and end your line with "the proved result so far is in
DIR/result-so-far.md". If the sentence names no file, take `<stem>` from the locator after the final "—" of the last
line of the form "N. PROVED: [GOAL] …" in DIR/ledger.md (grep) and use `DIR/<stem>.answer.md`, or
`DIR/<stem>.partial.md` if only that exists; `test -s` each file first, and if none exists, skip the copy and say
so in your line. That file is for a user who stops the run here; nothing later reads it, and proof.md remains the
run's deliverable. (On a problem that fixes its claim a raise never happens — there is nothing to raise to — so
the file is never written; a replacement is still announced.)
In every case record in state.md the number R of the last round whose wave actually ran (R = r after (c)–(d)
complete; when the loop is left at round r before its wave, R = r−1; R = 0 if no wave ever ran). The DRAFT BRIEF
needs it.
**(c) Wave.** Run the wave of the round's query files (see Rules: one worker per file — `math-proof-worker` in rounds
before ESC_ROUND, `math-proof-worker-deep` from round ESC_ROUND on —, all in one message, the script's `answers` verdicts, index lines, one
re-run of the queries not answered, then the FLOOR stop rule).
**(d) Screen (no launch).** There is no separate screening step: the next round's plan judge screens this wave's
answers itself (PLAN BRIEF, item 0) and writes DIR/judge/screen_r{r}.md; step (b) of the next round copies its
verdicts into the index. Update state.md ("phase: round {r+1} plan, attempt 1"; R = r) and continue the loop.
## The proof tail (after the loop ends, by CONCLUDE, TAIL, or finishing round MAX_ROUNDS)
First fix the tail's shape: run `SCRIPT gate DIR`. If its output begins `CONCLUDE`, the claims ledger holds the
headline goal settled and certified by two separate verify queries, and the tail is SHORT: (e) draft, (f) no refine step, no select step — build DIR/r3_verify.md yourself by the shell concatenation described under (g) and
write no r3_q files —, (h) a commit wave consisting of DIR/r3_verify.md alone, (i) finalize. If it prints
anything else (normally `REJECT: …`), the tail is FULL: steps (e)–(i) exactly as written below — except that a line
beginning `ERROR:` means the gate command itself was malformed (DIR first, as an absolute path): correct it and run
it again before deciding. Record "tail: short" or "tail: full" and
the gate's line in state.md. Two fallbacks guard the short tail. If its verify-only wave ends, after the one re-run, with no
DIR/r3_verify.answer.md, switch to the FULL tail from (g) on (note "tail: short, then full — no verify answer"). And if the
FIRST finalize reply of the short tail begins "MAIN CLAIM: NOT PROVED" (check this before the stand-alone grep check of
step (i)), the certified chain did not survive the verify query — note "tail: short, then full" in state.md,
rename DIR/r3_verify.md and (if it exists) DIR/r3_verify.answer.md to DIR/r3_verify.first.md / DIR/r3_verify.first.answer.md,
and likewise any DIR/r3_verify.partial.md to DIR/r3_verify.first.partial.md (appending " | renamed r3_verify.first" to the r3_verify index line), and run (g), (h) and (i) once more as in the FULL tail (the select judge then sees the finalize judge's proof.md
and, by the name in the index, the first verify report); this fallback applies at most once, and the second pass carries
(i) to the end whatever its reply's first line says.
**(e) Draft.** One `math-proof-judge` with the DRAFT BRIEF ({R} from state.md; {PARTIALS} is the text given after the
DRAFT BRIEF when the tail is FULL and R ≥ ESC_ROUND, and empty otherwise — SHORT tail, or R < ESC_ROUND; if R = 0 replace the brief's "final round's
results" clause by "(no wave completed before the rounds ended — work from the summary and ledger)") →
DIR/proof.md. The extra-query rule applies (see Rules; that relaunch, if it happens, is part of this step). If
DIR/proof.md does not exist once the step is over, launch the draft judge one more time with the added first
paragraph "DIR/proof.md was not written; write it now from the material named below."; if it still does not
exist, stop and report.
**(f) Refine**, REFINE_STEPS times in the FULL tail (step names refine_2, refine_3, … in order, REFINE_STEPS of them), not at all in the SHORT
tail: one `math-proof-judge` each with the REFINE BRIEF (extra-query rule applies, once per step).
**(g) Select.** One `math-proof-judge` with the SELECT BRIEF → up to MAX_COMMIT files DIR/r3_q{k}.md and exactly one
DIR/r3_verify.md. If DIR/r3_verify.md does not exist afterwards, create it with the shell, without retyping
anything, as the concatenation of: the lines "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.", a blank line, the line "## The draft proof", a blank line, and the file DIR/proof.md.
**(h) Commit wave.** Run every DIR/r3_q{k}.md (there are none in the SHORT tail) plus DIR/r3_verify.md as one
wave (no screen step for this wave).
**(i) Finalize.** One `math-proof-judge` with the FINALIZE BRIEF ({PARTIALS_FIN}: the text given after the FINALIZE BRIEF
when the tail is FULL and R ≥ ESC_ROUND, empty otherwise) → the final DIR/proof.md. Then the stand-alone
check: run `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`
(plain file handling; you are not reading the mathematics; no output means proof.md is clean). If it prints anything, proof.md still points at run
files a referee cannot open: launch the finalize judge ONCE more with the FINALIZE BRIEF preceded by the added
first paragraph "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.", note
"standalone-check: resent" in state.md, and accept whatever proof.md that launch leaves (do not repeat the check).
Update state.md ("phase: finished"). Reply to the user with: where proof.md is,
how many rounds ran and why the loop ended (the script's verdict line), how many worker queries ran, how
many were answered and how many ended partial, whether the goal was ever replaced or raised (one line, from
state.md; if DIR/result-so-far.md exists, say that it holds the earlier result as the worker wrote it, checked
only as far as the goal-change line recorded, and that proof.md and its Status section supersede it), and the judge's Status paragraph from its finalize reply, quoted. Do not
restate or assess the mathematics yourself.
## Rules that hold throughout
- Every judge step and every worker is a NEW subagent launch (the Agent tool) with `subagent_type` set
explicitly; never omit it. The sub-agents ship with this plugin and your agent list normally shows them under
plugin-scoped names — `math-proof:math-proof-judge`, `math-proof:math-proof-worker`, `math-proof:math-proof-worker-deep`.
Decide the name seat by seat: for each of the three, use the bare name (`math-proof-judge`, `math-proof-worker`,
`math-proof-worker-deep`) if your agent list offers it, otherwise the scoped name; mixing the two forms is fine (a
bare-named copy in the user's or the project's agents directory is how a user changes that one seat's settings,
and is meant to win). If one of the three is listed under neither name, tell the user that the math-proof
plugin's sub-agents are not in this session's agent list — open `/plugin` to check that math-proof is installed
and enabled, restart Claude Code, and give the same /math-proof:siege line again — and stop before round 1.
Record in state.md the name used for each seat. Judge steps use `math-proof-judge`. Workers — round waves and their re-runs — use `math-proof-worker` in rounds
before ESC_ROUND and `math-proof-worker-deep` in round ESC_ROUND and every later round; the workers of the proof
tail (extra-query waves, the commit wave, r3_verify) use `math-proof-worker-deep` if a wave ran in round ESC_ROUND
or later (R ≥ ESC_ROUND in state.md) and `math-proof-worker` otherwise. The choice is purely by round number, never
by your own view of how the attempt is going. Never reuse, resume or send a message to an earlier subagent.
Do not pass a `model` to the Agent tool: judges and workers run on this session's model.
Launch a whole wave in ONE message so the workers run in parallel; never run a subagent in the background.
- In every brief and worker prompt below, DIR stands for the run directory's absolute path and the other
{bracketed} slots for the values named; substitute them and send the text otherwise VERBATIM. Do not add
encouragement, hints, opinions about the problem, deadlines, or summaries of results to any brief or prompt.
- One fixed addition to EVERY `math-proof-judge` launch: after the brief, append a blank line,
the line "Problem statement (for reference — DIR/problem.md is the authoritative text; go by the file wherever
this copy differs or looks garbled):" and then the complete contents of DIR/problem.md, byte for byte (you read
it during setup). It is reference material so the judge's first request already contains
the problem; it changes no instruction in the brief, and the briefs' rule that the judge must not copy the
problem statement into query files still stands; DIR/problem.md, which every brief names, remains the authoritative
text. (Worker prompts carry the same text, in the fixed form given below.) Paste it exactly: copy the text you
read from DIR/problem.md character for character, never from memory and never retyped.
- You never write or edit query files, answer files (finished or partial), summaries, ledger files, notes.md or
proof.md yourself. The only files you write are state.md, index.md, the problem copy, the fallback r3_verify.md
and result-so-far.md (both by copying or concatenation only); beyond that you only copy or move files where a
step says so (cp/mv: summary.md, and the r3_verify.first renames in the proof tail). You do not read answer files beyond confirming they exist (`test -s`);
which of them are finished is decided by the bookkeeping script (`SCRIPT answers`, below), never by you.
- Worker prompts are always exactly this, with {Q} the query file stem (for example round2_q3, extra_q1,
r3_q2, r3_verify), {PROBLEM} the complete contents of DIR/problem.md, byte for byte, and {EARLIER} an empty
line — except when launching a query that this wave's latest `answers` run reported "partial", where {EARLIER} is the paragraph
given after this prompt, with an empty line before it and after it:
"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}, when not empty, is exactly: "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."
The end line is how a finished answer is told from one a worker was cut off in the middle of (by a usage
limit, an error or its turn limit); the bookkeeping script checks for it, you never do.
- Running a wave of query files means: launch one worker of the type this wave uses (`math-proof-worker` or
`math-proof-worker-deep`, see the first rule) per file, all in one message. When all have returned — never earlier: a worker still running is still
writing its file — run `SCRIPT answers DIR {Q1} {Q2} …` with the stems of the wave's query files, as a
command on its own, and read what it prints before you write any index line or launch anything. It decides,
without your reading anything, which answer files are finished, and prints one line per query — "{Q}: answered" (DIR/{Q}.answer.md ends with that query's end line: its worker
finished it), "{Q}: partial" (a worker wrote something but never finished; the script has moved that
unfinished file to DIR/{Q}.partial.md, so that a .answer.md file always means a finished answer) or "{Q}: no
answer" — and then a line "TOTAL (n queries): …" with the three counts (if it prints an ERROR line instead,
it is safe to correct the command — DIR first, then stems such as round2_q1 — and run it again).
Append to DIR/index.md ONE line per query: "{Q} | answered | ", "{Q} | partial | " or "{Q} | no answer | "
as the script said, followed by the first 300 characters of the worker's reply to you (its abstract — not the
answer file's contents), with newlines replaced by spaces so the entry stays on a single line. Then, if — and
only if — some query of the wave is not answered, relaunch a fresh worker for each such query (once, all in
one message; launch nothing for answered queries; a partial query's prompt carries the {EARLIER} paragraph,
which hands the new worker the unfinished file), and when they have all returned run `SCRIPT answers` again
with ALL the wave's stems (answered queries are unaffected), and append to the existing index line of each re-run
query (with the Edit tool; no second line for the query)
" | re-run: answered | ", " | re-run: partial | " or " | re-run: no answer | "
as it now reports, followed by the first 300 characters of the new worker's reply as before (a query cut off twice stays partial; the script keeps the
longer of its two unfinished files as DIR/{Q}.partial.md and the other beside it as DIR/{Q}.partial.prev.md).
So an index line reads "{Q} | status | abstract", sometimes followed by " | re-run: status | abstract", and
the re-run's status, when there is one, is the one in force; the plan, draft, refine and finalize briefs tell
the judges what a partial file is. Never launch a worker for a query
between a worker's return and the `answers` run that accounts for it. Note the TOTAL line of the last `answers` run for the wave — the one
over all its stems, so its count n equals the wave's size: the FLOOR rule below and state.md use it.
- No user will answer you during this session: never end your turn to ask how to proceed, never wait for confirmation, and
never stop early because something went wrong — decide by these rules and keep going until the protocol is
finished or a rule below says to stop. A subagent that returns an error, an interrupted result or an empty
reply is recorded in index.md / state.md and the protocol carries on; one lost worker is normal; a judge step
that comes back errored or interrupted is relaunched once immediately. If the same judge step fails (errors out, or writes none of its files) twice in a
row, stop and report where things stand. If, once a round's wave has ended after its one re-run,
answered + partial on that last TOTAL line is smaller than the FLOOR number the script printed with its WAVE
verdict (screening verdicts do not count against this), stop and report: something systematic is wrong and
continuing would only spend judge steps on nothing — tell the user the likeliest cause is a usage limit or an
outage that cut the workers off, that the run's files are intact, and that giving the same /math-proof:siege line
again in this directory resumes the run once the cause has cleared. (If that TOTAL line's n is smaller than the wave, you ran
`answers` on only some stems — run it on all of them first.) The extra-query and commit waves have no floor.
- Extra queries: when a draft or refine brief allows it, the judge may write up to 3 files named
DIR/extra_q{k}.md using the next unused numbers k; the whole run has a budget of 10 (once DIR/extra_q10.md
exists, no more may be written — the briefs say so). When a judge's reply says it wrote extra query files,
confirm they exist, run them as a wave (their answers land in DIR/extra_q{k}.answer.md, or in
DIR/extra_q{k}.partial.md for one cut off twice — the index says which), then relaunch that same step ONCE
with this added first paragraph: "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." A second
batch of extra files from the relaunched step is left on disk unanswered.
- Rewrite DIR/state.md after every step: protocol, settings, current phase, attempt counters, and a growing
one-line-per-step log; each round's plan line also records the wave cap passed to the check command and each
wave's line the worker type launched and the last TOTAL line (e.g. "cap 10, math-proof-worker-deep ×9, answered 8,
partial 1, no answer 0"). It is your only memory if this conversation is ever compacted; if you find yourself
unsure where you are, read state.md and ${CLAUDE_SKILL_DIR}/SKILL.md again.
## PLAN BRIEF (round {r} of at most {MAX_ROUNDS}; {CAP}, {HORIZON}, {CONCLUDE_RULE}, {ESC_SUMMARY} and {ESC_WAVE} depend on r, see (a) and below)
> Step: plan round {r} of at most {MAX_ROUNDS}.{HORIZON} Files: the problem is DIR/problem.md; your running notes are
> DIR/notes.md; the running summary from the previous round is DIR/summary.md (absent in round 1); the claims
> ledger is DIR/ledger.md (absent or empty until something is recorded); the previous round's results are the
> files DIR/round{r-1}_q*.answer.md whose line in DIR/index.md gives the status "answered" (each line reads
> "query | status | abstract", sometimes followed by "| re-run: status | abstract", and then the re-run's
> status is the one that holds; none in round 1), plus DIR/extra_q*.answer.md if any exist. A query whose
> status is "partial" has instead a file DIR/round{r-1}_q{k}.partial.md: the notes of an engine that was cut
> off part-way. Read it too, for leads and for material to build new queries on, but nothing in it is
> established — it can prompt an OPEN line or a query, never by itself a PROVED line (one exception: if it
> holds a complete written proof or refutation of the [GOAL] claim, or of an earlier goal, since raised, that
> the audit rule below still covers, that proof counts as "in hand" for the audit rule exactly as if the file were
> finished — you also write the settled [GOAL] line that the audit and conclusion rules call for, with that
> query's stem (e.g. round3_q2) as its locator — and the verify queries then decide).
> (Every finished result file ends with a bookkeeping line "=== END OF ANSWER … ===": it is not part of the
> mathematics; leave it out of anything you splice or quote.) Read the problem, your notes, the summary, the
> ledger and the index first, then the previous round's result files — each file once, in full.
>
> 0. Screen first (rounds 2 and later). As you read the previous round's result files, check that each is a
> genuine attempt at its query — not a refusal, an empty or near-empty file, off-topic text, or work on a
> different problem. Write DIR/judge/screen_r{r-1}.md with one line per query of that round, exactly
> "round{r-1}_q{k}: OK" or "round{r-1}_q{k}: DEGENERATE: one-line reason" ("DEGENERATE: no answer" for a query
> whose status is no answer; a partial query's .partial.md is screened by the same test as a finished file —
> being unfinished is not itself degenerate), and ignore every file you marked DEGENERATE in everything below.
> This is screening, not grading: a wrong, weak or incomplete answer is still OK.
>
> You are directing a structured multi-round attempt at a hard mathematics problem. Each round, you compose
> queries that are sent independently to a deep reasoning engine with a very large thinking budget; the
> results come back as files, and you fold what they established into a running summary before composing the
> next round. This is round {r} of at most {MAX_ROUNDS}.{HORIZON} {CONCLUDE_RULE}
>
> Do these three things, in order.
>
> 1. Update the running summary. Rewrite it from scratch into DIR/round{r}_summary.md: it REPLACES the
> previous summary and is the only memory later rounds (and the final proof assembly) have of what came
> before, so carry forward everything still relevant. Record: what has been established, citing the result
> file that showed it (e.g. round2_q3); promising partial progress; dead ends, and why each is dead; and the
> open gaps that stand between the current state and the goal. Be honest — an overclaimed summary poisons
> every later round. Keep it under 6000 words. Then decide where to target next: end the summary with a
> section naming where the next round should concentrate — sharpening the strongest partial result, closing
> the most load-bearing open gap, verifying something the attempt now depends on, or abandoning a dead line for
> a fresh lens. Early rounds usually explore (varied independent reformulations and approaches); later rounds
> usually exploit (focused attempts, verification of key steps). The choice is yours each round.{ESC_SUMMARY}
>
> 2. Update the claims ledger. Alongside the summary, the run keeps a numbered ledger of claims, each marked
> PROVED, REFUTED, or OPEN. Unlike the summary, the ledger is never rewritten: the lines you write now are
> APPENDED verbatim (the numbering is added for you), and an existing entry is removed from force only by
> appending an explicit RETRACT line naming its number. Write DIR/round{r}_ledger_block.md containing ONLY this
> round's new lines, one per line, each of the form "PROVED: one-sentence claim — locator", "REFUTED:
> one-sentence claim — locator", "OPEN: one-sentence claim — locator" (locator = the result file stem, e.g.
> round2_q3), or "RETRACT 4: one-sentence reason entry 4 no longer stands". Append a line for every
> load-bearing claim this round settled or opened, a new line for any claim whose status changed (the newest
> line for a claim supersedes older ones), and a RETRACT line for anything now known wrong. Keep lines to one
> sentence: the full ledger is carried verbatim into every later round and into the final proof assembly — it
> is the one memory of this attempt that cannot fold away. Tag the line that states the headline goal with
> [GOAL] right after the status word ("PROVED: [GOAL] …", "OPEN: [GOAL] …"), and tag with [AUDIT] a PROVED
> line recording that a separate verify query checked a complete written proof chain (name that query's
> locator and cite the entry it certifies as "entry N" or "#N"). Tag lines as they arise. In round 1 write
> exactly one [GOAL] line. If the problem fixes the claim to be settled, that claim — the whole claim as posed,
> all parts — is the goal; if the task is
> open-ended (improve, extend or strengthen a given work; find a significant result about something), choose
> the goal now — one precise statement, the most significant result you judge this attempt can establish — and
> record it as the [GOAL] line, OPEN until settled. (i) Status lines. Write a further [GOAL] line for the same
> claim only when its status changes (OPEN → PROVED or REFUTED, or back to OPEN when a verify query finds a
> gap — then also RETRACT the PROVED line) — and then in the very round whose result files first contain the
> complete written proof, so that the verify queries you compose in the same step certify a line that is
> already numbered when their answers return — or to come back to it under (iv) below; never merely to re-word
> it, since only the newest [GOAL] line counts, and an [AUDIT] line must cite by number the [GOAL] entry it
> certifies, which is the newest one when the goal has not moved since (lines in your block are numbered on from
> the last entry of DIR/ledger.md, in file order). (ii) Changing the goal. The goal is not fixed: at any later plan step you may set a new goal by writing a new OPEN [GOAL] line, which is the
> goal from then on (this is no reason to aim low in round 1: choose the round-1 goal exactly as above);
> throughout this brief, "the [GOAL] line" and "the [GOAL] claim" mean the newest [GOAL] line in force and its
> claim. There are two reasons to set a new goal. Replace the goal (RETRACT the old [GOAL] line — if it was
> PROVED and the proof stands, re-enter what it proved as an ordinary untagged PROVED line — then write the new
> one) if it turned out false, ill-posed or already known, and also if you find it is narrower than, or
> different from, the claim the problem itself poses — then the posed claim is the new goal (a replacement, not
> a raise, even when the narrower goal was already PROVED: on a problem that fixes its claim the run's verdict is
> about that claim); for a goal you chose yourself in round 1 on an open-ended task, a refutation means replace it and continue (for a goal you raised to, see (iii)), and a
> REFUTED [GOAL] line ends the run only when the problem itself posed that claim. Or raise the goal: once the
> current goal is PROVED, if a more significant result now looks within reach of the rounds that remain — a
> stronger statement, or the general case of what was proved — write the new statement as an OPEN [GOAL] line
> (locator roundN_plan, N being this round's number), held to the same standard as the round-1 choice (one
> precise statement that you judge this attempt can establish, not one that as far as you can tell is false,
> ill-posed or already known). A raise is always an OPEN line: never write as a PROVED [GOAL] line a claim
> stronger than what the result files actually prove. When the problem itself posed the claim and it is proved
> as posed, there is nothing to raise to: conclude. (iii) What a raise leaves in place. When you raise, do not retract the proved goal or its
> [AUDIT] lines: they stay in force as ordinary entries, and that result is what the final document presents if
> the raised goal is not reached. If instead a verify query finds a gap in the proof of the goal you raised away
> from, RETRACT its PROVED [GOAL] line — never leave in force a PROVED [GOAL] line whose proof has failed its
> check — and decide afresh under (ii) which statement is the goal (to return to the earlier one, write it as the
> newest OPEN [GOAL] line and aim the wave at the gap). A REFUTED raised goal is not the run's verdict, and its
> refutation needs no verify queries (the audit rule below is for a goal the run may conclude on): record it as a
> "REFUTED: [GOAL] …" line naming the refuting file, then re-state the goal you proved below it, as (iv)
> describes, and conclude on that. Raising is a judgment, not a duty: if nothing clearly more significant looks
> within reach, conclude on the proved goal under the rule on concluding given earlier in this brief; and if the
> first two waves aimed at a raised goal (the raising round's own wave is the first) leave it no nearer — no
> proof of it, and no new route to one — then at the next plan step come back to the goal already proved and
> conclude. Coming back takes precedence over the summary's chain and progress rules and the escalation rule
> below, which direct a wave at a stalled statement only while it stays the goal: a step that comes back
> composes no queries other than any verify queries the audit rule still requires for the goal it returns to (one audit wave, then
> conclude). Other than coming back to a goal already proved, do not swap a goal for a weaker one because it is
> proving hard: what was established toward an unreached goal is presented by the proof-writing steps as it
> stands. Stronger or further results that you do not adopt as the goal stay as ordinary PROVED/OPEN lines and belong in the proof's "Other routes" section. (iv) Coming back. To come back to
> a goal proved earlier (the raised statement did not yield), re-state it in this round's block as a "PROVED:
> [GOAL] …" line citing its earlier entry as "entry N" or "#N", placed after any other [GOAL] line the block
> holds so that it is the newest (lines are numbered in file order), and below it re-state its certifications as
> [AUDIT] lines, each naming its verify query's locator as before and citing the new line's number in the same
> form (count it: if DIR/ledger.md ends at entry 23 and the re-stated goal is the second line of your block, it
> is entry 25) — one such line suffices when the re-stated goal line cites the earlier entry, otherwise two, from
> separate queries; then conclude under the rule on concluding. Leave the file empty if no claim was settled,
> opened, changed, or retracted.
>
> 3. Compose the next round's queries — or conclude. If and only if the material in hand fully establishes
> the goal, write DIR/round{r}_DONE.md containing one line naming where the material establishes it, and write
> no queries (if you raise the goal in this step, compose a wave for it instead — never write
> DIR/round{r}_DONE.md in the same step as a raise). Otherwise write between 1 and {CAP} query files DIR/round{r}_q1.md, DIR/round{r}_q2.md, …
> (consecutive numbers) aimed at the target you chose. While the [GOAL] line is OPEN, parallel queries are
> cheap and independent, so prefer using most of the budget; make them genuinely different attempts at the
> target, not rewordings of one attempt. Once a complete written proof (or refutation) of the [GOAL] claim is in
> hand, the wave shrinks: compose the verify queries the audit rule below requires plus at most 2 others, aimed
> at what the final proof document will need (a corollary's full write-up, the proof of a lemma that was only
> cited, an independent second proof). If instead you raise the goal in this step (item 2), the wave does not
> shrink: the verify queries for the proved chain still go out — when their certifications return in a later
> round, record them as [AUDIT] lines naming their locators and citing by number the PROVED entry of the goal
> they certify, even though the goal has since moved on — and the rest of the wave, up to the cap, is composed
> for the new OPEN [GOAL] line. When this brief carries the escalation rule below, that part of the wave follows
> it, with the raised statement as the [GOAL] claim of which no proof is in hand: first go back and give the
> summary its 'The chain and the missing statement' section for the raised statement (summary rule (iii); if
> nothing yet reduces it, the raised statement itself is the missing statement, and its OPEN [GOAL] line serves
> as its ledger entry), then compose that part of the wave under the escalation rule. Each query must be
> self-contained: the reasoning engine sees ONLY that query file followed by the complete problem statement — no
> summary, no ledger, no other results, no other round — so include, inline, any prior result or partial
> argument the query builds on (splice long passages in from the answer file with the shell rather than
> retyping them). Do NOT copy the problem statement itself into any query.
> Targeting rule (applies every round). Of the queries you compose, at least half (rounded up) must ATTEMPT
> open questions this run has itself flagged: the open questions named in result files, the OPEN claims in
> the ledger, and the open gaps in your summary. Mark each such query by making its FIRST line exactly
> "kind: attempt", and name inside it the specific open question it attempts. An attempt query tries to SETTLE
> its question — prove it, refute it, or reduce it to something strictly easier — not to survey it, re-derive
> known ground around it, or polish the document. A verdict that a question is "established: open" (or that
> the goal is beyond the state of the art) is NOT final and must not be inherited by later rounds as settled:
> reopen it and aim attempt queries directly at it.
> Audit rule (applies every round). Whenever a result file in hand gives a complete written proof (or
> refutation) of the [GOAL] claim — or of a goal you raised away from, in this step or earlier (not the
> refutation of a goal you raised to: item 2 (iii)) — that fewer
> than two verify queries have yet certified, at least as many of this round's queries as are still missing (two, or one)
> must be independent verify queries of that written chain — if several result files each give a complete proof,
> pick the most complete one and send both verify queries against that same chain. Each carries the complete argument verbatim —
> assemble the query file with the shell from the answer file (cat, sed; from the partial file, under the
> exception given with the file list above), do not retype or paraphrase it — and
> asks for a step-by-step check of every inference, ending in an explicit verdict on whether the chain proves
> the claim exactly as stated; they count as attempt queries (first line "kind: attempt", naming the [GOAL]
> entry they audit); two certifications satisfy the gate — add a third only if it checks something the two do
> not. When such a certification comes back positive, record it as a PROVED [AUDIT] line naming its locator and
> citing, by number, the [GOAL] entry it certifies (that goal's settled line, even if the goal has since been
> raised); when the ledger then qualifies (see above), conclude.{ESC_WAVE}
> Retrieval rule. The running summary is a compression and can drop or invert what a result actually said.
> Whenever you rely on or contradict a prior result — in the summary rewrite, in a ledger line, in your target
> choice, or in a decision to conclude — first read that result's answer file and work from what it actually
> says, not from the summary's paraphrase of it.
>
> Finally rewrite DIR/notes.md, and reply in under 150 words: concluded or not, how many query files and how
> many of them are attempt queries, and the target in one sentence. If you replaced, raised or came back to a
> goal this round (item 2), add one more sentence, not counted in the 150 words, beginning "Goal change:" —
> which of the three, what the goal was and what it is now (each in a short phrase), and the result already
> proved if one stands, with its ledger entry number and how many verify queries have certified it so far; for a
> raise, also name by full path the answer file or files that hold that result's complete proof (form: "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} is, when r < MIN_ROUNDS, exactly: "You may conclude in this round, before round {MIN_ROUNDS},
as soon as the claims ledger holds the headline goal settled — a PROVED or REFUTED line tagged [GOAL] ("PROVED:
[GOAL] …") — and at least two PROVED lines tagged [AUDIT]. Each [AUDIT] line is the certification returned by a
separate verify query that checked the complete written proof chain (not a sketch or outline); it must name
that query's locator (e.g. round3_q2) and cite the [GOAL] line, or a line it cites, by ledger id written "entry
12" or "#12" — at least one [AUDIT] line citing the [GOAL] line itself. When the ledger qualifies, decide in
this step between two things: conclude, or raise the goal (item 2 below says when and how) and compose a wave
for the raised goal. Do not run further waves merely to reach round {MIN_ROUNDS} or to polish — the
proof-writing steps that follow do the polishing. Tag lines as they arise. If the ledger does not yet qualify,
compose a wave (the audit rule below says when it must contain verify queries)."
— and when r ≥ MIN_ROUNDS it is exactly: "From this round on you may conclude whenever the material in hand
fully establishes the [GOAL] claim — except that if a complete written proof is in hand that fewer than two verify queries
have yet certified, the audit rule below still applies this round (one audit wave, then conclude) — and when such a proof is in hand,
this round's ledger block must already carry the [GOAL] line settled, written in the ledger's ordinary form
"PROVED: [GOAL] …" (or "REFUTED: [GOAL] …") with nothing between the status word and the tag — that it is not
yet certified needs no mark of its own, the [AUDIT] lines record certification —, in the same step that composes
its verify queries. Once the [GOAL] claim is established you either conclude (after its audit wave, where the
audit rule applies) or raise the goal (item 2 below; a raise need not wait for the audits), never both in one
step: a step that raises the goal writes no DONE file, since a raised goal is settled by a wave, not by concluding. If you raised the goal in an earlier round and
the raised statement has not yielded, you may conclude on the goal already proved, re-stating it as the newest
[GOAL] line as item 2 (iv) describes. In the final round, do that rather than letting the rounds simply run out."
{HORIZON} is empty when r ≤ MAX_ROUNDS−2; when r = MAX_ROUNDS−1 it is exactly: " So at most one further round
can run after this one." and when r = MAX_ROUNDS exactly: " So this is the final round: whatever its queries
return goes straight to the proof-writing steps, with no further round to act on it." (Note the leading space.
{MAX_ROUNDS} in the brief is the MAX_ROUNDS setting written as a number, every round.)
{ESC_SUMMARY} is empty when r < ESC_ROUND; when r ≥ ESC_ROUND it is exactly (leading space included):
" From this round on four further rules govern the summary; because rule (iii) asks you for mathematics of your
own, write the summary file with its carried-forward material and (i)–(ii) before working (iii) out, then extend
it — a message spent only thinking can be cut off and what was not written is lost. (i) Standing results: keep a
section of that name listing every PROVED ledger line that is a theorem about the problem in general (all parameters), an exact
reformulation or reduction of the [GOAL] claim to a named simpler or classical statement, or a complete
solution of a natural special case — each with its locator — even when it cannot by itself finish the goal;
never drop an entry from this section (mark it 'not on the current line' instead), because if the goal is not
reached the final document is built around these. (ii) Dead ends: a route is dead only by a precise statement
that was REFUTED and the result file that refuted it, and is recorded in exactly that form. One result file
reporting an obstruction, a failed search inside one ansatz or one candidate, or that a route reaches only part
of the goal, closes that candidate, not the route: list such routes under the open gaps as 'set aside, not
refuted', open to re-attack. (iii) The chain and the missing statement. First decide whether a complete written
proof or refutation of the [GOAL] claim is in hand. A result file that proves last round's missing statement
exactly as stated, when that chain needs nothing further, IS one: in that case record the [GOAL] line PROVED (or
REFUTED, for a disproof) in this round's ledger block, citing by number the entries the chain uses and naming the
new proof's locator, and compose the audit rule's verify queries so that they carry the WHOLE chain — the cited
entries' arguments and the new proof, each spliced from its answer file, joined by the chain's derivation exactly
as last round's summary states it. If a complete written proof or refutation is in hand, that way or any other,
skip the rest of (iii) and all of (iv). Otherwise the summary carries a section headed exactly 'The chain and the
missing statement', rewritten every round, with four labeled parts. Chain: the derivation by which the [GOAL]
claim (or its negation, when the line pursued is a disproof — then read 'proof of the missing statement' below
accordingly) follows from results already PROVED — cited by ledger
number, statements only — together with exactly ONE further statement not yet proved; write the derivation out
step by step, so that a reader holding the cited entries and a proof of that one statement would hold a complete
proof. If the material does not yet reduce the goal to a single statement, take as the missing statement the
strongest intermediate claim the main line needs next, and say in the chain what would still remain after it.
Missing statement: that one statement written out in full and self-contained — every quantifier, every object
defined, and every hypothesis of the problem it may use stated with it (a statement stripped of a hypothesis it
actually needs becomes false, and its refutation then discredits a sound line). It may carry hypotheses of its
own — a restriction to some of the objects or to part of the parameter range — only if the chain shows, citing
PROVED entries, that everything outside those hypotheses is already settled; a statement whose proof would still
leave some of the objects the problem admits unsettled is a special case, not the missing statement. Among
statements that would complete the chain prefer the simplest and most concrete. Enter it in the ledger as an
OPEN line (as locator write roundN_plan, N being this round's number) the first time you state it and whenever
its wording changes — and then also RETRACT the OPEN line of the wording it replaces — so that later rounds and
queries can refer to it. Why it should hold: your own sketch, in at most fifteen lines, of why you believe it and
by what kind of argument it could be proved — do this mathematics yourself: if you can see a candidate mechanism,
of whatever kind, that would give it, state it precisely; a conjecture of yours that the engines then prove or
refute is among the most useful things this step produces. Tried so far: one line per query already spent on
this statement or an earlier wording of it — locator, the approach it took, and what it yielded (a proof of a
special case, an equivalent reformulation, an obstruction, nothing); identical copies of one task share a line;
an approach so listed counts as tried. (iv) Progress test. Open the target section by saying whether the last two
rounds produced progress on the chain, counting as progress ONLY: a proof of the missing statement; a proof of the
[GOAL] claim; a new PROVED result that holds for every object the hypotheses admit and shortens the chain; or the
replacement of the missing statement by a strictly simpler one (simpler, not merely narrower), with the chain
re-derived. Settling a further part of the objects while the hard part of the missing statement stays open — so
that the statement merely narrows — or an equivalent reformulation of it, is recorded under (i) but is not
progress in this sense. If there was none, write 'main line stalled — no universal progress', say in one line
what in your sketch or decomposition differs from last round's, and do not respond by opening another special
case or by turning to other routes for breadth: the wave (unless item 2 (iii) now has you come back to a goal
already proved and conclude) goes to the missing statement itself under the Closing rule below, and what must change is your own sketch in (iii) — a different mechanism for the same statement, or
a different decomposition of the chain with a different missing statement. If a result file REFUTED the missing
statement exactly as stated, do not rescue it merely by excluding the counterexample's class (unless a PROVED
entry already settles that class, and the chain says so): either state a corrected missing statement and
re-derive the chain for it in full, or record the line as dead under (ii) and build the chain of the next most
promising line. From this round on, 'verifying' as a target means only the audit rule's goal audits and the one
chain check the Closing rule's item (c) allows."
{ESC_WAVE} is empty when r < ESC_ROUND; when r ≥ ESC_ROUND it is exactly (leading space included; {CAP} substituted
as elsewhere):
" Escalation rule (this round and every later one, for as long as no complete written proof or refutation of
the [GOAL] claim is in hand — once one is, including the case summary rule (iii) describes of a proved missing
statement that completes the chain, the audit rule and the shrunken wave above take over, and (a)–(c) below are
then ignored). The engines answering this round have a much larger thinking budget than those of the opening
rounds, and the wave may hold up to {CAP} queries: use most of it, and spend it on the missing statement of your
chain, stated in full — not on surveys, and not on breadth for its own sake. (a) Every query attacks: it attempts
the missing statement, the [GOAL] claim itself, or a question whose answer would settle or strictly reduce one of
them (settling it for part of the objects only is not a reduction). Do not spend queries on writing up,
polishing, re-deriving or verifying results that do not complete the [GOAL] chain — the proof-writing steps
after the rounds do that, with their own query budget — so the only verify queries in a round are the audit
rule's (the verify queries certifying a goal that was proved and then raised count as the audit rule's) and
the one chain check item (c) allows. Do not spend a query asking an engine to recall or reconstruct a
proof from the literature, of the [GOAL] claim or of anything else: the engines have no library to consult, and
such a task gives them nothing to reason with (invoking known theorems inside an attack is another matter, and
fine). (Only in the final two rounds — this brief's opening 'Step: plan round …' line will then say so
explicitly, in the words "one further round" or "the final round"; if it carries neither, this is not one of
them — up to two queries may instead verify, or write up in full, the standing results the final document will
present.) (b) Closing rule.
Write ONE task file that asks for a complete proof of exactly the missing statement of your chain — or else an
explicit counterexample to it — and that contains: the statement, verbatim as the summary states it; every prior
result it may rest on, spliced in full with its proof from the answer files (cat, sed — never paraphrased); the
chain's derivation of the [GOAL] from it, so that the engine sees what the statement is for and can say so if
that derivation is itself flawed; your sketch of why it should hold, offered as a suggestion the engine is free
to discard; and the explicit sentence that a proof of the statement for only some of the cases it covers — a
sub-class of its objects or a sub-range of its parameters — does not answer the question, though it should be
reported if it is all that was found. Save it as this round's query file q1 (the first of the files named above)
and copy it byte for byte (cp) to q2 and q3: three engines attempt the same statement independently —
independent attempts at one well-posed statement are worth more here than one attempt each at three statements.
These identical copies are intended (the instruction above against rewordings of one attempt does not apply to
them), and all three are attempt queries (first line 'kind: attempt', naming the missing statement as the open
question they attempt). (c) The remaining queries — use most of the cap — also go to the missing statement, each
self-contained (carrying the same splices unless said otherwise below), and each is either a further
byte-for-byte copy of the closing task (allowed: it is one more independent attempt) or genuinely different from
it: an attack by a named approach that does not appear under 'Tried so far' (name it in the task; the engine may
depart from it if it says why); or a listed approach continued from the partial result it returned, with that
result spliced in; or the hardest single step of your own sketch, cut out and posed as a self-contained claim; or
the one obstruction a result file raised against the statement, posed as the thing to overcome or to sharpen into
a counterexample. In the first round a missing statement is posed, and again whenever its wording has changed,
one of these queries instead tries to REFUTE it exactly as stated — by an explicit construction, or by deriving
from it something known to be false. When the same missing statement has already been attacked in two earlier
rounds, one of these queries is given only the statement and the cited entries' statements (no proofs, no
sketch), and is asked first to derive for itself that the statement would complete the [GOAL] and then to attack
it by a first move none of the listed attempts used — an engine that finds the derivation does not go through,
or the statement implausible, says so, and that is a result to act on under summary rule (iv). At most TWO
queries of the wave may go elsewhere: to routes the main line does not descend from (set aside, not refuted,
under summary rule (ii)), or —
at most one of them — to checking one PROVED step the chain rests on that no separate query has yet checked. All
of these are attempt queries (first line 'kind: attempt')."
## DRAFT BRIEF
> Step: proof draft. Files: the problem is DIR/problem.md; your running notes are DIR/notes.md; your running
> summary of everything the attempt established is DIR/summary.md; the claims ledger is DIR/ledger.md; the
> final round's results are the newest DIR/round{R}_q*.answer.md files marked answered and not DEGENERATE in
> DIR/index.md; every earlier round's result files and DIR/extra_q*.answer.md are there to consult by name (a
> DIR/…_q{k}.partial.md file, where the index marks a query partial, is the unfinished and unverified notes of
> an engine that was cut off: leads only, nothing in it is established; and the "=== END OF ANSWER … ===" line
> that closes each finished file is bookkeeping, not mathematics).
> Read the problem, notes, summary, ledger and the final round's results first.
>
> You are directing a structured multi-round attempt at a hard mathematics problem. The rounds have concluded.
> Your job now: write DIR/proof.md containing the strongest route to the goal — the most complete argument the
> attempt found — with its full argument spelled out,{PARTIALS} plus a short note on every other route worth recording,
> and an honest statement of anything that remains a gap — a clearly-marked gap is worth more than a
> papered-over one. If the newest [GOAL] line is not PROVED — or is PROVED but not certified by two [AUDIT]
> lines and its written proof does not survive your own check — and the ledger holds, in force, a PROVED [GOAL]
> line for a different claim (a goal that was reached and then raised; if several, the most recent), then that
> proved goal is proof.md's main claim. State it as the document's theorem and write its complete argument out
> in full from the result files the ledger names for it (where the file the ledger names is a .partial.md file,
> take the text from the verify query files that carried it and whose answers certified it); it is not one of the
> lesser results. The raised goal
> comes after it, as a statement that was attempted, with whatever was established toward it, and the Status
> section says which is which. Use python3 whenever a concrete computation would confirm or kill a step: check a
> candidate identity on examples, verify a constant, test a claimed counterexample numerically. Checking beats
> believing. If one or a few targeted deep-reasoning queries would settle a load-bearing point, you may write
> them as the next unused DIR/extra_q{k}.md files (at most 3 in this step; none once DIR/extra_q10.md exists),
> each self-contained — the engine sees only that file followed by the problem statement, so include inline
> whatever it builds on and do not copy the problem into it — and say in your reply that you did; they will be
> answered and you will be invoked once more. Write DIR/proof.md in this step regardless. Rewrite
> DIR/notes.md. Reply in under 150 words.
{PARTIALS} is empty in the SHORT tail and whenever R < ESC_ROUND; in the FULL tail with R ≥ ESC_ROUND it is
exactly (leading space included): " 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 (step name {S} = refine_2, refine_3, … in order)
> Step: {S}. Files: the problem is DIR/problem.md; your running notes are DIR/notes.md; the current draft is
> DIR/proof.md; the result files are DIR/round*_q*.answer.md (every round's results) and DIR/extra_q*.answer.md,
> listed with their status in DIR/index.md (a query whose status there is "partial" has instead a
> DIR/…_q{k}.partial.md, the unfinished and unverified notes of an engine that was cut off: leads, not results;
> and the "=== END OF ANSWER … ===" line that closes each finished file is bookkeeping, not mathematics); the
> claims ledger is DIR/ledger.md and the running summary DIR/summary.md.
> Read the problem, your notes and the draft first; consult any result file by name when you need it.
>
> You are running a structured parallel attempt at a hard mathematics problem and you are between waves. Your
> job this step: make proof.md strictly better. Re-derive the weakest steps, hunt for errors as a hostile
> referee would, and use python3 to check every concrete computational claim you rely on. If one targeted
> deep-reasoning query would settle a load-bearing gap, you may write it as the next unused DIR/extra_q{k}.md
> (at most 3 in this step; none once DIR/extra_q10.md exists), self-contained — the engine sees only that file
> followed by the problem statement, so include inline whatever it builds on and do not copy the problem into
> it — and say in your reply that you did. Then rewrite DIR/proof.md in full, first saving the incoming draft as
> DIR/judge/{S}_previous_proof.md. Be honest about what remains a gap — a clearly-marked gap is worth more than
> a papered-over one. Rewrite DIR/notes.md. Reply in under 150 words.
## SELECT BRIEF
> Step: select routes for the commit wave. Files: the problem is DIR/problem.md; your running notes are
> DIR/notes.md; the draft proof is DIR/proof.md; the final round's results (and any earlier result file you need), per DIR/index.md (a query marked "partial" there has only unverified notes in a DIR/…_q{k}.partial.md, from an engine cut off part-way); the claims ledger DIR/ledger.md.
>
> You are running a structured parallel attempt at a hard mathematics problem; you have a draft proof document
> and the full results of the pursuit. Your job is the commit step of the protocol: any result with a concrete
> route (a named lemma chain, a specific construction) toward the goal gets a commit query at the full thinking
> budget: "Route: [the route]. Write the full rigorous proof." Plus one verify query that checks the draft
> proof's argument step by step. (If a goal was proved and a later, raised goal was not, the draft's main claim
> is the proved goal; concrete routes toward the raised goal may still be committed.)
> Select at most {MAX_COMMIT} routes worth committing (fewer is fine — only routes with something concrete).
> For each, write the query as DIR/r3_q1.md, DIR/r3_q2.md, …, with the route's actual content included (not a
> reference to it — the engine sees nothing but the query file followed by the problem statement). Do NOT copy
> the problem statement into any query. Also write exactly one DIR/r3_verify.md containing the complete
> current draft proof (copied in full from DIR/proof.md with the shell — cat —, not retyped) and asking for a step-by-step check: for every
> inequality, interchange, cited result and "it follows that", does it actually follow as written; list every
> error or gap in order of severity and say explicitly whether the main claim is proved.
> Use python3 if a quick computation would settle which routes are real. Rewrite DIR/notes.md. Reply in under
> 100 words with the list of files written.
## FINALIZE BRIEF
> Step: finalize. Files: the problem is DIR/problem.md; your running notes are DIR/notes.md; the draft proof
> that went into the commit wave is DIR/proof.md; the commit-wave results are DIR/r3_q*.answer.md and the
> verify query's report is DIR/r3_verify.answer.md (DIR/index.md says which exist; if none exist, finalize from
> the draft; a query the index marks "partial" has instead a DIR/r3_q{k}.partial.md or DIR/r3_verify.partial.md,
> the unfinished notes of an engine that was cut off — unverified, so a proof in one is a lead to check, not a
> result, and the gaps a cut-off verify report lists are still worth checking, though the absence of its final
> verdict tells you nothing either way; the "=== END OF ANSWER … ===" line closing each finished file is bookkeeping); the claims ledger is
> DIR/ledger.md. Read all of these.
>
> You are running a structured parallel attempt at a hard mathematics problem. The commit wave has returned.
> Your job is the final step of the protocol: assemble the final proof.md from the best commit result (or from
> the draft if no commit query produced better). Iterate: if the verify query found gaps, repair what is
> repairable from the material you have; use python3 to check every concrete computational claim you rely on.
> Be honest in the final document about anything that remains a gap — a clearly-marked gap is worth more than a
> papered-over one. The final document must state the problem's answer and give the complete argument, then a
> short section "Status" saying plainly whether the main claim is fully proved and listing anything that
> remains a gap, and a short section "Other routes" on anything else worth recording{PARTIALS_FIN}. If the
> newest [GOAL] line is not PROVED — or is PROVED but not certified by two [AUDIT] lines and its written proof
> does not survive the verify report and your repairs — and the ledger holds, in force, a PROVED [GOAL] line for
> a different claim (the goal was raised after being reached; if several, the most recent), then the main claim
> is that proved goal, stated and proved as the document's theorem, not presented as a lesser result. The raised
> goal is reported after it as attempted, not as a gap in the main claim, and the Status section says plainly
> which claim is the main claim and that the raised goal was not reached. proof.md is read on its
> own by a referee who cannot open any other file in this directory: never cite run files (r*_q*, extra_q*,
> *.answer.md, the verify report, notes, scripts) in it; write every relied-on argument out in full in
> proof.md, rewriting it from the worker files if needed. Save the incoming draft
> as DIR/judge/finalize_previous_proof.md first, then write the final DIR/proof.md. Rewrite DIR/notes.md. Reply
> in under 200 words: first a line beginning exactly "MAIN CLAIM: PROVED" or "MAIN CLAIM: NOT PROVED" (your
> Status section's verdict on proof.md's main claim as defined above; PROVED here means the document's main
> result — a proof, or a disproof, of that claim — is complete), then on the same line a dash and that main
> claim in one clause, then that Status paragraph.
{PARTIALS_FIN} is empty in the SHORT tail and whenever R < ESC_ROUND; in the FULL tail with R ≥ ESC_ROUND it is
exactly (leading space included): " (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)"
plugins/math-proof/skills/siege/scripts/ledger.py
Executable
+662
View File
@@ -0,0 +1,662 @@
#!/usr/bin/env python3
"""Bookkeeping helper for the math-proof plugin's siege skill: the four mechanical
decisions of the round loop and its waves that should not depend on a
model's judgment.
ledger.py check DIR R WAVE MIN_ROUNDS ATTEMPT
After the round-R plan step: validates the shape of what the judge
wrote, applies the early-conclusion gate, commits the round's ledger
lines (numbered on) to DIR/ledger.md once the round's plan is final,
and prints ONE verdict line for the orchestrator:
WAVE <n> FLOOR <f> run round R's wave (files roundR_q1.md .. roundR_q<n>.md);
stop the run if fewer than <f> of its queries come
back answered or partial
CONCLUDE <why> leave the round loop
RETRY: <text> relaunch the plan step with <text> as an added
first paragraph (ATTEMPT < 3 only)
TAIL: <why> give up on this round and go to the proof tail
ledger.py append DIR R
Number the lines of DIR/roundR_ledger_block.md on from the ledger of
rounds before R, write DIR/roundR_ledger.md, rebuild DIR/ledger.md.
Idempotent (safe to re-run for the same round).
ledger.py gate DIR [R]
Print CONCLUDE or "REJECT: <reason>" for the early-conclusion gate on
the assembled ledger as it stands (plus round R's not-yet-appended
block, numbered on, when R is given).
ledger.py answers DIR Q1 [Q2 ...]
After a wave's workers have all returned: decide which answer files
are finished. A worker that finishes writes the end line
"=== END OF ANSWER <Q> ===" last; a file without it was cut off. For
each query stem Q (e.g. round2_q3) prints "Q: answered" (DIR/Q.answer.md
ends with Q's end line), "Q: partial" (only an unfinished file exists)
or "Q: no answer", then one TOTAL line with the number of queries and
the three counts. Side effects, so that a .answer.md file always means
a finished answer: an unfinished DIR/Q.answer.md is moved to
DIR/Q.partial.md (if an older, longer Q.partial.md is already there,
that one stays and the new file goes to Q.partial.prev.md instead; a
shorter older one moves to Q.partial.prev.md), and an empty
DIR/Q.answer.md is deleted. Nothing a worker wrote is ever deleted or
overwritten except an older Q.partial.prev.md. Idempotent; an ERROR
line (and nothing touched) if a stem is wrong.
A malformed command (DIR not an existing directory, a missing or non-numeric
argument) prints an ERROR line and touches nothing. Standard library only
(Python 3.7 or later); files are read and written as UTF-8 regardless of the
platform's default encoding. Always exits 0 and says what it decided on
stdout; any internal error prints a fail-closed verdict (RETRY/REJECT, or an
ERROR line from `answers`) rather than a traceback the orchestrator might
misread.
"""
from __future__ import annotations
import re
import sys
from pathlib import Path
MAX_ATTEMPTS = 3 # plan attempts per round before a shortfall is accepted
ENC = dict(encoding="utf-8", errors="replace")
# ---- ledger parsing and the early-conclusion gate --------------------------
_LEDGER_STATUS_WORDS = ("OPEN", "PROVED", "REFUTED", "RETRACT", "RETRACTED", "SKETCHED")
_SETTLED = ("PROVED", "REFUTED")
def _take_tags(text: str, tags: set) -> str:
"""Strip a leading cluster of short bracketed tags ("[GOAL] ",
"[AUDIT]: ") off text, adding each (upper-cased) to tags; a
bracketed STATUS word is not a tag and stops the scan. Tags count
only in this leading position — a prose mention later in the line
("the key step toward [GOAL]") is not a tag."""
while True:
m = re.match(r"^[*_\s]*\[([A-Za-z]{1,6})\]\s*[:\-–—]?\s*", text)
if not m or m.group(1).upper() in _LEDGER_STATUS_WORDS:
return text
tags.add(m.group(1).upper())
text = text[m.end() :]
def _cited_ids(text: str) -> set:
"""Ledger-id citations in an entry's free text. Two forms count:
the word forms ("entry 12", "line 12", "claim 12", "item 12",
"no. 12", and hybrids like "entry L5" — case-insensitive, the
same family the RETRACT target parser tolerates) and the "#12"
form. A prose "L12" deliberately does NOT count: every
prose-position L-number matcher tried was fail-open on analysis
prose — "in L2", "the L2 norm", "L2(R)", and coordinated lists
like "verified the L1 and L2 bounds" collide exactly with the
small ids early-round goals get. The plan brief and the RETRY
correction teach the counted forms, so a judge writing
"cites L12" is re-asked and can correct — a missed citation only
costs a retry (fail-closed), where a spurious one ends a paid run
early. Decimal and slash-fraction references never count ("Claim
2.4 of the draft", "line 1/2" — ledger ids are integers), and the
L hybrid ("entry L5") is not accepted after "line"/"lines", where
it collides with geometry prose ("lines L2 and L4 are tangent").
Bare integers are never citations (math prose is full of them)."""
ids = set()
for m in re.finditer(r"#(\d{1,4})\b(?![./]\d)", text):
ids.add(int(m.group(1)))
for m in re.finditer(
r"\b(?:entry|entries|claim|claims|item|items|id|ids|no\.|number)"
r"\s+#?L?(\d{1,4})\b(?![./]\d)"
r"|\b(?:line|lines)\s+#?(\d{1,4})\b(?![./]\d)",
text,
re.IGNORECASE,
):
ids.add(int(m.group(1) or m.group(2)))
return ids
def ledger_entries(ledger_text: str) -> dict[int, dict]:
"""Parse the assembled numbered ledger ("12. OPEN: claim — locator",
"13. RETRACT 4: reason") into {n: {status, text, retracted_by,
goal, audit}}. Tolerant of what judges actually write after the
number this script assigns: a self-assigned id ("L3.", "(L5)", "#7:"),
markdown emphasis around the status word ("**OPEN**:"), any case,
and RETRACT spelled "RETRACTED" / aimed at "L4", "#4", "entry 4" or
"claim 4". status is upper-cased (PROVED / REFUTED / OPEN / RETRACT
/ whatever other word the judge used); retracted_by is the number
of the RETRACT line that removed the entry from force, if any.
goal/audit are set only by a [GOAL]/[AUDIT] tag in tag position —
immediately before or after the status word — never by a prose
mention elsewhere in the line."""
out: dict[int, dict] = {}
for ln in ledger_text.splitlines():
m = re.match(r"\s*(\d+)\.\s+(.*)", ln)
if not m:
continue
n, rest = int(m.group(1)), m.group(2)
# a self-assigned id is dropped only when punctuated or bracketed
# ("L3." / "L3:" / "(L3)" / "#3:"), so prose like "L2 norm" survives
rest = re.sub(
r"^[*_\s]*(?:\(\s*(?:L|#)?\s*\d+\s*\)\s*[.:\-–—]?|(?:L|#)\s*\d+\s*[.:)\-–—])\s*",
"",
rest,
)
tags: set = set()
rest = _take_tags(rest, tags)
sm = re.match(
r"[*_\s\[]*([A-Za-z]+)[*_\]]*\s*[:.\-–—]?\s*(.*)", rest, re.DOTALL
)
if not sm:
continue
status, text = sm.group(1).upper(), sm.group(2)
if status.startswith("RETRACT"):
status = "RETRACT"
text = _take_tags(text, tags)
out[n] = {
"status": status,
"text": text,
"retracted_by": None,
"goal": "GOAL" in tags,
"audit": "AUDIT" in tags,
}
for n, e in out.items():
if e["status"] == "RETRACT":
tm = re.match(
r"[*_\s]*(?:entry|claim|item|line|no\.?|number)?\s*[#(]?\s*L?\s*(\d+)",
e["text"],
re.IGNORECASE,
)
if tm and int(tm.group(1)) in out and int(tm.group(1)) != n:
out[int(tm.group(1))]["retracted_by"] = n
return out
def early_conclude_ok(entries: dict[int, dict], known_locators=None) -> bool:
"""Early-conclusion gate. True when the ledger's goal is settled and
twice audited:
- the NEWEST in-force [GOAL]-tagged line is PROVED or REFUTED (the
ledger's own supersession rule: a later unsettled [GOAL] update
takes the goal back out of play without needing a RETRACT);
- at least two in-force PROVED [AUDIT] lines — the goal line itself
never counts as its own audit, byte-duplicate lines count once —
each cite the goal line, or a line its text cites, by ledger id
("entry 12" / "#12"; a prose "L12" does not count — see
_cited_ids; ids must resolve to existing entries), and at least
one cites the goal line itself;
- when known_locators is given (check and gate pass the stems of the
result files that actually exist), each counted audit line must
name one — matched case-insensitively, since the files are all
lowercase while a judge may title-case at sentence start — and
the counted audits must span at least two distinct locators,
tying the certifications to queries that really ran, from at
least two separate queries.
REFUTED settles a prove-or-disprove goal as surely as PROVED (an
audited disproof concludes the run). One consequence of the
cite-the-goal requirement, by design: audits recorded before the
[GOAL] line existed (or before a [GOAL] re-statement) cite older
ids and so cannot satisfy it — append-only history is never
implicitly re-tagged — and the concluding plan's own ledger block
must re-state at least one certification citing the goal line's
id (the RETRY correction names this fix). The gate is a structured
attestation check on judge-written ledger text, not an independent
proof check: the run's correctness still rests on the audits being
real, which the locator requirement grounds but cannot prove."""
live = {n: e for n, e in entries.items() if e["retracted_by"] is None}
goals = sorted(n for n, e in live.items() if e.get("goal"))
if not goals:
return False
g = goals[-1]
if live[g]["status"] not in _SETTLED:
return False
chain = {g} | {m for m in _cited_ids(live[g]["text"]) if m in live}
audits = []
seen = set()
for n in sorted(live):
e = live[n]
if e["status"] != "PROVED" or not e.get("audit") or e.get("goal") or n == g:
continue
cites = _cited_ids(e["text"]) & chain
if not cites:
continue
norm = " ".join(e["text"].split()).lower()
if norm in seen:
continue
locs = None
if known_locators is not None:
locs = {
loc
for loc in known_locators
if re.search(
rf"(?<![A-Za-z0-9_]){re.escape(loc)}(?![A-Za-z0-9_])",
e["text"],
re.IGNORECASE,
)
}
if not locs:
continue
seen.add(norm)
audits.append((n, cites, locs))
if len(audits) < 2:
return False
if not any(g in cites for _, cites, _ in audits):
return False
if known_locators is not None:
spanned = set().union(*(locs for _, _, locs in audits))
if len(spanned) < 2:
return False
return True
# ---- end of ledger parsing and the gate -----------------------------------
def _round_of(p: Path) -> int:
m = re.fullmatch(r"round(\d+)_ledger", p.stem)
return int(m.group(1)) if m else -1
def _parts(d: Path) -> list:
return sorted(
(p for p in d.glob("round*_ledger.md") if _round_of(p) >= 0), key=_round_of
)
def ledger_text(d: Path, before=None) -> str:
"""The assembled ledger: the per-round numbered parts, in round order."""
out = []
for p in _parts(d):
if before is not None and _round_of(p) >= before:
continue
out.append(p.read_text(**ENC))
return "".join(out)
def numbered_lines(d: Path, r: int, block: str) -> list:
"""Round r's new lines, numbered on from the ledger of rounds < r, with
the judge's bullets / numbering / self-assigned ids stripped."""
prior = ledger_text(d, before=r)
n = sum(1 for ln in prior.splitlines() if ln.strip())
lines = []
for raw in (block or "").splitlines():
ln = re.sub(r"^(?:[-*]|\d{1,4}\.)\s+", "", raw.strip())
ln = re.sub(
r"^(?:\((?:L|#)?\d{1,4}\)(?:[.:]\s*|\s+)|(?:L|#)\d{1,4}[.:]\s+)(?=\S)",
"",
ln,
)
if ln:
n += 1
lines.append(f"{n}. {ln}")
return lines
def append(d: Path, r: int) -> int:
bp = d / f"round{r}_ledger_block.md"
block = bp.read_text(**ENC) if bp.exists() else ""
lines = numbered_lines(d, r, block)
(d / f"round{r}_ledger.md").write_text(
"".join(f"{ln}\n" for ln in lines), encoding="utf-8"
)
(d / "ledger.md").write_text(ledger_text(d), encoding="utf-8")
return len(lines)
def known_locators(d: Path) -> set:
return {p.name[: -len(".answer.md")] for p in d.glob("*.answer.md")}
def gate_reason(text: str, locs: set) -> str:
"""'' when the early-conclusion gate passes on this ledger text, else
the first failing condition in plain words (the pass/fail decision
itself is early_conclude_ok's)."""
entries = ledger_entries(text)
if early_conclude_ok(entries, locs):
return ""
live = {n: e for n, e in entries.items() if e["retracted_by"] is None}
goals = sorted(n for n, e in live.items() if e.get("goal"))
if not goals:
return "the ledger has no [GOAL]-tagged line in force"
g = goals[-1]
if live[g]["status"] not in _SETTLED:
return f"the newest [GOAL] line (entry {g}) is {live[g]['status']}, not PROVED or REFUTED"
audits = [
n
for n, e in live.items()
if e["status"] == "PROVED" and e.get("audit") and not e.get("goal") and n != g
]
if len(audits) < 2:
return f"only {len(audits)} PROVED [AUDIT] line(s) in force besides the goal line (entry {g}); two are needed"
return (
f"the [AUDIT] lines do not yet form a qualifying pair: each must cite the [GOAL] line "
f"(entry {g}) or a line it cites as 'entry N' or '#N' (at least one citing entry {g} itself), "
f"each must name the locator of an answer file that exists (e.g. round3_q2), and together "
f"they must come from two different queries"
)
def round_queries(d: Path, r: int) -> list:
qs = [
p for p in d.glob(f"round{r}_q*.md") if re.fullmatch(rf"round{r}_q\d+", p.stem)
]
return sorted(qs, key=lambda p: int(p.stem.rsplit("_q", 1)[1]))
def is_attack(p: Path) -> bool:
"""kind: attempt declared near the top (first three non-empty lines that
contain letters — tolerates a front-matter fence or a heading first)."""
seen = 0
for ln in p.read_text(**ENC).splitlines():
if not re.search(r"[A-Za-z]", ln):
continue
if re.match(
r"[*_\s`#>-]*kind[*_`\s]*[:=][\s\"'*_`]*(attempt|attack)", ln, re.IGNORECASE
):
return True
seen += 1
if seen >= 3:
return False
return False
def is_withdrawn(p: Path) -> bool:
"""An emptied or '(withdrawn)' query file left over from a re-plan."""
t = p.read_text(**ENC).strip()
return not t or bool(
re.fullmatch(r"[(\[]?\s*withdrawn\s*[)\]]?\.?", t, re.IGNORECASE)
)
def wave_floor(n: int) -> int:
"""Fewest queries of a round's wave that may come back answered or
partial before the run stops (3 in 10 of the wave, rounded down, and at
least 1)."""
return max(1, (3 * n) // 10)
_STEM = re.compile(r"[A-Za-z0-9_]+")
def is_end_line(line: str, stem: str) -> bool:
"""True when line is the end line of query `stem`, "=== END OF ANSWER
<stem> ===", compared tolerantly: any case; the '=' rails in any
length or absent, or drawn with other symbols; markdown dressing (a
heading '#', a quote '>', a list marker, a wrapper or inner emphasis of
backticks, asterisks, underscores or quotes, an escaped underscore
'round2\\_q3'); a colon after ANSWER; a final period; and the stem given
bare, as "<stem>.md", as "<stem>.answer.md" or as a plain path ending in
one of those; a checklist item ("- [ ] ...") never counts. What must
survive is exactly the words END OF ANSWER followed by this query's own
name and nothing else: an end line copied in from another query's text
(spliced into a task file by the judge, say) names that other query, and
a sentence that merely mentions the end line has other words around it;
neither counts."""
if re.search(r"\[[ xX]\]", line): # a checklist item is a plan, not an end line
return False
t = line.replace("\\_", "_")
t = re.sub(r"[^A-Za-z0-9_./ -]+", " ", t) # drop rails, emphasis, quotes
t = " ".join(t.split()).strip("_- ")
t = re.sub(r"^\d{1,2}\. ", "", t) # a numbered-list marker
name = rf"(?:[A-Za-z0-9_./-]*/)?{re.escape(stem)}(?:\.answer\.md|\.md)?"
return bool(re.fullmatch(rf"END OF ANSWER {name} ?\.?", t, re.IGNORECASE))
_TAG_ONLY = re.compile(r"(?:\s*</?[A-Za-z_][\w:.-]*\s*/?>)+\s*")
def _last_line(text: str) -> str:
"""The last line of text that contains a letter or digit ('' if none),
so that a closing code fence or a rule drawn under the end line does
not hide it. A line made of nothing but bare markup tags without
attributes (a stray '</details>' or similar closing tag a model sometimes
emits after its last real line) is skipped the same way: a worker does not
write its end line in that form, and skipping such a line can only
reveal an end line the worker did write above it."""
for ln in reversed(text.splitlines()):
if not re.search(r"[A-Za-z0-9]", ln) or _TAG_ONLY.fullmatch(ln):
continue
return ln
return ""
def answers(d: Path, args: list) -> str:
"""Classify each query's answer file and set unfinished ones aside (see
the module docstring). Only one line of DIR/Q.answer.md is looked at, the
last that contains a letter or digit and is not a bare markup tag;
nothing else in any file is read for meaning."""
stems, seen = [], set()
for arg in args:
stem = Path(arg).name # tolerate a path or a file name for a stem
for suffix in (".answer.md", ".partial.md", ".md"):
if stem.endswith(suffix):
stem = stem[: -len(suffix)]
break
if not _STEM.fullmatch(stem):
return f"ERROR: {arg!r} is not a query stem (letters, digits and underscores only, e.g. round2_q3, extra_q1, r3_q2, r3_verify); nothing was touched"
if not any((d / f"{stem}{x}").exists() for x in (".md", ".answer.md", ".partial.md")):
return f"ERROR: there is no query file {stem}.md in {d} (wrong DIR, or a mistyped stem); nothing was touched"
if stem not in seen:
seen.add(stem)
stems.append(stem)
out, counts = [], {"answered": 0, "partial": 0, "no answer": 0}
for stem in stems:
a, p = d / f"{stem}.answer.md", d / f"{stem}.partial.md"
status = None
if a.exists():
text = a.read_text(**ENC)
if is_end_line(_last_line(text), stem):
status = "answered"
elif not text.strip():
a.unlink() # an empty file is no answer; any older partial stays
elif p.exists() and p.stat().st_size > len(text.encode("utf-8", "replace")):
# an older, longer unfinished file stays the partial; keep this one beside it
a.replace(d / f"{stem}.partial.prev.md")
else:
if p.exists() and p.read_text(**ENC).strip():
p.replace(d / f"{stem}.partial.prev.md")
a.replace(p)
if status is None:
partial = p.exists() and p.read_text(**ENC).strip()
status = "partial" if partial else "no answer"
counts[status] += 1
out.append(f"{stem}: {status}")
out.append(
f"TOTAL ({len(stems)} {'query' if len(stems) == 1 else 'queries'}): answered {counts['answered']}, partial {counts['partial']}, no answer {counts['no answer']}"
)
return "\n".join(out)
GATE_RULE = (
"Concluding before round {m} requires the claims ledger to hold the headline goal settled "
"as a PROVED or REFUTED line tagged [GOAL], plus at least two PROVED lines tagged [AUDIT] "
"from two separate verify queries, each naming its query's locator (e.g. round3_q2) and "
"citing the [GOAL] line or its chain by ledger id written 'entry 12' or '#12', at least one "
"citing the [GOAL] line itself. Only the newest [GOAL] line counts, it never counts as one of "
"its own audits, and audits recorded before that line cite older ids — re-state the "
"certifications citing its id (one suffices when the [GOAL] line itself cites the line they "
"certify; otherwise two, from separate queries). Either compose a wave — for example verify "
"queries whose certifications complete the chain — or conclude once the ledger qualifies."
)
STILL_THERE = (
" The files from your previous attempt at this round (summary, ledger block, notes, any query "
"files) are still in place and this round's ledger block has NOT been appended to DIR/ledger.md "
"yet: rewrite DIR/round{r}_ledger_block.md so that it holds ALL of this round's new ledger lines, "
"and if you now conclude instead of composing a wave, delete this round's query files "
"(DIR/round{r}_q*.md) first — existing query files take precedence over a conclusion."
)
def check(d: Path, r: int, wave: int, min_rounds: int, attempt: int) -> str:
"""The round-r plan verdict. The round's ledger block is committed to
ledger.md only together with a terminal verdict (WAVE / CONCLUDE /
TAIL), never on RETRY — so a re-planned round simply rewrites its block,
and the early-conclusion gate is evaluated on the ledger of earlier
rounds plus this attempt's not-yet-appended lines."""
final = attempt >= MAX_ATTEMPTS
wave = max(1, wave)
sp = d / f"round{r}_summary.md"
if not sp.exists() or not sp.read_text(**ENC).strip():
what = f"no running summary (DIR/round{r}_summary.md is missing or empty)"
return (
f"TAIL: {what} after {attempt} attempts"
if final
else f"RETRY: Correction — the previous attempt at this step wrote {what}. "
f"Write DIR/round{r}_summary.md, then EITHER DIR/round{r}_DONE.md OR between 1 and {wave} query files."
+ STILL_THERE.format(r=r)
)
qs = round_queries(d, r)
for p in [q for q in qs if is_withdrawn(q)]:
p.replace(p.with_name(p.stem + ".withdrawn.md"))
qs.remove(p)
for k, p in enumerate(qs, 1): # close gaps so the wave is q1..qn
want = d / f"round{r}_q{k}.md"
if p != want:
p.replace(want)
qs[k - 1] = want
done = d / f"round{r}_DONE.md"
if qs: # composed queries take precedence over a verdict
if done.exists():
done.replace(d / f"round{r}_DONE.superseded.md")
extra = ""
if len(qs) > wave:
for p in qs[wave:]:
p.replace(p.with_name(p.stem + ".overcount.md"))
qs = qs[:wave]
extra = f"; over-count: files beyond q{wave} set aside"
need = (len(qs) + 1) // 2
got = sum(1 for p in qs if is_attack(p))
if got < need and not final:
return (
f"RETRY: Correction — the previous plan step composed {len(qs)} queries but marked only {got} "
f"with a first line 'kind: attempt'; at least {need} (half, rounded up) must be attempt queries "
f"aimed at this run's own flagged open questions, each beginning with the line 'kind: attempt' "
f"and naming the open question it attempts. Rewrite the query files DIR/round{r}_q1.md … "
f"(overwrite them; if you now compose fewer, delete the surplus files with rm) so that the wave "
f"satisfies this." + STILL_THERE.format(r=r)
)
n_new = append(d, r)
note = f", kind=attempt {got}/{len(qs)}" + (
" accepted below quota after retries" if got < need else ""
)
return (
f"WAVE {len(qs)} FLOOR {wave_floor(len(qs))} (ledger +{n_new}{note}{extra})"
)
if done.exists() and done.read_text(**ENC).strip():
if r >= min_rounds:
n_new = append(d, r)
return f"CONCLUDE (round {r} >= floor {min_rounds}; ledger +{n_new})"
bp = d / f"round{r}_ledger_block.md"
pending = numbered_lines(d, r, bp.read_text(**ENC) if bp.exists() else "")
text = ledger_text(d, before=r) + "".join(f"{ln}\n" for ln in pending)
why = gate_reason(text, known_locators(d))
if not why:
n_new = append(d, r)
return f"CONCLUDE (audited chain accepted before round {min_rounds}; ledger +{n_new})"
if final:
n_new = append(d, r)
return f"CONCLUDE (accepted before round {min_rounds} after {attempt} plan attempts without a qualifying chain — {why}; ledger +{n_new})"
done.replace(d / f"round{r}_DONE.rejected{attempt}.md")
return (
f"RETRY: Correction — your conclusion at round {r} was not accepted: {why}. "
+ GATE_RULE.format(m=min_rounds)
+ STILL_THERE.format(r=r)
)
what = f"neither DIR/round{r}_DONE.md nor any query file DIR/round{r}_q1.md …"
if final:
n_new = append(d, r)
return f"TAIL: {what} after {attempt} attempts (ledger +{n_new})"
return (
f"RETRY: Correction — the previous attempt at this step wrote {what}. The required shape is: "
f"DIR/round{r}_summary.md, then EITHER DIR/round{r}_DONE.md (only if the goal is fully established) "
f"OR between 1 and {wave} query files. Write exactly that."
+ STILL_THERE.format(r=r)
)
USAGE = (
"usage: ledger.py check DIR R WAVE MIN_ROUNDS ATTEMPT | append DIR R | gate DIR [R] | "
"answers DIR Q1 [Q2 ...] (bookkeeping for the math-proof siege skill; DIR is the run directory)"
)
# per command: its usage form, then how many arguments follow DIR (at least,
# at most) and how many of those must be whole numbers
_FORMS = {
"check": ("check DIR R WAVE MIN_ROUNDS ATTEMPT", 4, 4, 4),
"append": ("append DIR R", 1, 1, 1),
"gate": ("gate DIR [R]", 0, 1, 1),
"answers": ("answers DIR Q1 [Q2 ...]", 1, None, 0),
}
def _malformed(argv: list) -> str:
"""'' when the command line has the right shape, else an ERROR line."""
cmd, rest = argv[1], argv[3:]
if cmd not in _FORMS:
return f"ERROR: unknown command {cmd!r}. {USAGE}; nothing was touched"
form, lo, hi, nints = _FORMS[cmd]
if len(argv) < 3 or len(rest) < lo or (hi is not None and len(rest) > hi):
return f"ERROR: usage: ledger.py {form} (DIR first, as an absolute path); nothing was touched"
d = Path(argv[2])
if not d.is_dir():
return f"ERROR: '{d}' is not an existing run directory; give the run directory's absolute path first (ledger.py {form}); nothing was touched"
if not all(a.isascii() and a.isdigit() for a in rest[:nints]):
return f"ERROR: usage: ledger.py {form}; the arguments after DIR must be whole numbers (got {' '.join(rest[:nints])}); nothing was touched"
return ""
def main(argv: list) -> str:
if len(argv) < 2 or argv[1] in ("-h", "--help"):
return USAGE
try:
bad = _malformed(argv)
if bad:
return bad
cmd = argv[1]
d = Path(argv[2])
if cmd == "append":
return f"APPENDED {append(d, int(argv[3]))}"
if cmd == "gate": # on ledger.md as it stands, plus round R's pending block if R given
text = ledger_text(d)
if len(argv) > 3:
r = int(argv[3])
bp = d / f"round{r}_ledger_block.md"
text = ledger_text(d, before=r) + "".join(
f"{ln}\n"
for ln in numbered_lines(
d, r, bp.read_text(**ENC) if bp.exists() else ""
)
)
why = gate_reason(text, known_locators(d))
return "CONCLUDE" if not why else f"REJECT: {why}"
if cmd == "answers":
return answers(d, argv[3:])
if cmd == "check":
r, wave, min_rounds, attempt = (int(x) for x in argv[3:7])
# the orchestrator's attempt count is advisory: every RETRY this
# script has already issued for round r is logged, so a confused
# caller passing attempt=1 forever still reaches the terminal
# verdicts after MAX_ATTEMPTS plan steps
logp = d / "judge" / f"plan_r{r}_retries.log"
issued = len(logp.read_text(**ENC).splitlines()) if logp.exists() else 0
attempt = max(attempt, issued + 1)
verdict = check(d, r, wave, min_rounds, attempt)
if verdict.startswith("RETRY"):
logp.parent.mkdir(parents=True, exist_ok=True)
with logp.open("a", encoding="utf-8") as f:
f.write(f"attempt {attempt}: {verdict[:120]}\n")
# corrections are pasted into a brief whose paths are absolute
return verdict.replace("DIR/", str(d).rstrip("/") + "/")
return USAGE
except Exception as e: # fail closed, in words the orchestrator can relay
if len(argv) > 1 and argv[1] == "answers":
return f"ERROR: the bookkeeping script could not classify the answer files ({type(e).__name__}: {str(e)[:200]}); check DIR and the query stems and run the command again"
attempt = 0
try:
attempt = int(argv[6]) if len(argv) > 6 and argv[1] == "check" else 0
except ValueError:
pass
err = f"the bookkeeping script could not process this round's files ({type(e).__name__}: {str(e)[:200]})"
if attempt >= MAX_ATTEMPTS:
return f"TAIL: {err}, still failing after {attempt} attempts"
return f"RETRY: Correction — {err}; re-check the file names and formats the brief asks for and write them again."
if __name__ == "__main__":
try: # the verdict goes out as UTF-8 whatever the console's code page (Windows)
sys.stdout.reconfigure(encoding="utf-8", errors="replace")
except (AttributeError, ValueError):
pass
print(main(sys.argv))
plugins/math-proof/skills/solo/SKILL.md
+69
View File
@@ -0,0 +1,69 @@
---
name: solo
description: "Work on one hard mathematics problem in this session yourself, with no sub-agents: reason in stages, record each settled step in a notes file so that nothing written is lost if a response is cut off, and end with a self-contained proof.md. Usage: /math-proof:solo <the problem, stated in full, or the path of a file holding it>."
argument-hint: "[DIR=run-directory] <problem statement | problem-file>"
disable-model-invocation: true
disallowed-tools: WebSearch, WebFetch, AskUserQuestion
allowed-tools: Read, Write, Edit, Glob, Grep, Bash(mkdir *), Bash(cp *), Bash(cmp *)
---
# math-proof: solo
You solve the problem yourself, in this session. There are no sub-agents and no rounds: just you, a notes
file and, at the end, proof.md.
**Arguments.** The invoking message reads: $ARGUMENTS
It gives the problem and, optionally, the run directory. Read it this way. A token of the form DIR=path at its
start sets the run directory (the path quoted if it contains spaces); remove it. Any other leading token of the
form NAME=value, where NAME is a word of two or more capital letters and underscores and value is a whole number,
is a setting this skill does not have: tell the user in one sentence that /math-proof:solo takes only DIR=path
before the problem (round and wave settings belong to /math-proof:siege), and that if the token is part of the
problem itself the problem can be given as a file path instead, and stop. If what remains is a single line
that, taken as a whole — surrounding whitespace and one pair of enclosing quotation marks removed,
backslash-escaped spaces read as spaces — is the path of an existing file (it may contain spaces; check with
Read or Glob, not the shell), that file is the problem file; if no such file exists and what remains can only
be a file path — a single line ending in .md, .txt or .tex, or a single token (no spaces once the quotes are
removed) containing "/" or "\" — tell the user in one sentence that no file exists at the absolute path you
looked for (give it) and that the problem can instead be given in full as text after the command, and stop;
otherwise everything that remains, to the end of the message, IS the problem statement, verbatim — mathematics,
line breaks and all ("n=3", "N=pq" and "AB=AC" are mathematics, not settings). The run directory DIR defaults to
./math-proof-solo under the current directory; use DIR's absolute path everywhere below. If the message holds
neither a readable problem file nor any problem text, say so in one sentence — with the usage,
`/math-proof:solo <problem statement, or the path of a file holding it>` — and stop.
**Setup.** The run's files are DIR/problem.md (the problem), DIR/notes.md (your notes) and DIR/proof.md (the
deliverable). Create DIR with `mkdir -p`. If DIR/notes.md already exists, this problem was already being
worked on in DIR: check that DIR/problem.md is the same problem you were given (compare the text, ignoring
differences in whitespace and line endings; for a file, `cmp`) — if it differs, say in one sentence that DIR
holds work on a different problem and that `DIR=<another directory>` selects a fresh one, and stop; if it is
the same, read DIR/notes.md, and DIR/proof.md if it exists. If they record the solution as complete (proof.md
written and nothing in the notes still to do), the earlier session finished: say where proof.md is and that
`DIR=<another directory>` starts a fresh attempt, and stop. Otherwise the earlier session ended before it
finished, and whatever reasoning it had not written down is lost: continue from the last point recorded there
rather than starting over. If DIR/notes.md does not exist yet, put the problem at DIR/problem.md: if it came as
a file, copy that file there byte for byte with `cp`; if it came as text in the invoking message, Write
exactly that text (nothing added, removed or reworded). Then Read DIR/problem.md in full; it is the authoritative text of the problem. Use the shell for
nothing but that `mkdir`, `cp` and `cmp`.
**The task.** Solve the problem stated in DIR/problem.md; the deliverable is DIR/proof.md. After reasoning,
write your answer. This task runs as a conversation that can span many messages, each with a bounded output
allowance; a message that is cut off is normally followed by a request to continue, and only what you have
WRITTEN (not unwritten reasoning) is guaranteed to carry into the next message. So write your work product
out as you go, in a notes file, DIR/notes.md: whenever you settle something — a lemma and its proof, a
reduction, a dead end and why it is dead, the precise statement you are now attempting — write it down before
reasoning further. A partial answer is much more useful than none. Writing to the notes is not finishing —
keep going after each write. Important: each message's output allowance also covers your private reasoning,
and it is far smaller than a hard problem deserves — a message spent entirely on reasoning, with nothing
written, gets cut off, and unwritten reasoning should be assumed lost. So do not try to finish in one
message. Work in stages: early in EVERY message, before any long derivation, write your current plan and the
precise statement you are attempting to DIR/notes.md; then reason toward the next concrete intermediate
result, append it to the notes as soon as you have it, and continue. Many short written steps beat one long
unwritten one. If a message of yours is cut off, re-read DIR/notes.md and continue from the last thing
written there; never start over. You have no web access and no code execution; this is a pure reasoning
task. When the problem is resolved, or you have taken it as far as you can, write your complete solution to
DIR/proof.md. proof.md is read on its own by a referee who cannot open any other file (not your notes
either), so it must be self-contained: every argument the solution relies on is written out in full there.
Work unattended: there is no one to answer questions, so never stop to ask.
When DIR/proof.md is written, reply briefly: where proof.md is, and whether it resolves the problem
completely or, in proof.md's own words, what it leaves open.