Experiment 1 · Design

Experiment 1: agents and verifiers on one lemma

Fix one lemma (§1), two rounds, the same agents throughout and $B=10^8$ tokens per run; vary only the team: $k\in\{1,2,4,8\}$ agents, of which none or half are verifiers. (a) Does splitting $B$ over more agents make a correct proof more likely? (b) At equal $k$, do verifiers leave fewer mistakes that the run itself never noticed? Both are read off the attempt tree each run leaves (§3, §4).

1. The problem: Lemma 7.2

From the Whittaker paper (draft, not public), §7.1; its proof there is a TODO.

(setting)

Geometry. Perfect schemes over $\mathbb F_q$, in mixed characteristic: every object below is a functor on perfect $\mathbb F_q$-algebras $R$, and Witt vectors $W_{\mathcal O}(R)$ replace the power series $R[[t]]$ of the equal-characteristic loop groups [Zhu, §1].

$F/W(\mathbb F_q)[1/p]$ finite totally ramified, ring of integers $\mathcal O$, uniformizer $\varpi$, $W_{\mathcal O}(R)=W(R)\otimes_{W(\mathbb F_q)}\mathcal O$; $G$ split reductive over $\mathcal O$, $B=TN$, opposite unipotent $N^-$.

$$\begin{aligned} L^nG(R)&=G\big(W_{\mathcal O}(R)/\varpi^n\big), && \text{a perfect affine group scheme},\\ L^+G(R)&=G\big(W_{\mathcal O}(R)\big)=\textstyle\varprojlim_n L^nG(R), && \text{a perfect affine group scheme},\\ LG(R)&=G\big(W_{\mathcal O}(R)[1/\varpi]\big), && \text{an ind-(perfect scheme)}, \end{aligned}$$ $$P_n=L^+G\times_{L^nG}L^nN,\qquad t_n=\check\rho_{\mathrm{ad}}(\varpi^{-n})\in T_{\mathrm{ad}}(F),\qquad \mathring I_n=\operatorname{ad}(t_n)(P_n)\subset LG,$$

$\langle\alpha,\check\rho_{\mathrm{ad}}\rangle=1$ for every simple root $\alpha$; $P_n(R)=\{g\in L^+G(R): g\bmod\varpi^n\in N\}$; $\operatorname{ad}(t_n)$ is conjugation through $G_{\mathrm{ad}}$.

(triangular decomposition; Lemma 7.2 of the paper)

For $0\lt n\lt\infty$, multiplication is an isomorphism of functors on perfect $\mathbb F_q$-algebras

$$(\mathring I_n\cap LN^-)\times(\mathring I_n\cap LT)\times(\mathring I_n\cap LN)\xrightarrow{\ \sim\ }\mathring I_n ,$$

the intersections taken in $LG$: for every perfect $R$, each $g\in\mathring I_n(R)$ is uniquely $u^-tu$ with the three factors in $\mathring I_n(R)$, naturally in $R$.

2. Experiment

2.1 Steps

Inputs. One folder with Definition 1, Lemma 2, the paper's §2 and §7.1 (proof of 7.2 removed) and Zhu §1, copied unchanged into every run.
Run list. $\mathcal C\times\{1,2\}$: 14 runs, in an order drawn once with a fixed seed (§2.3).
Pilot. One run of $(1,\text{off})$ in each harness, exp1-cc-pilot (Claude Code; run 30 October 2026, report on the private branch) and exp1-cx-pilot (Codex), before the 14 and outside them: each tests run_exp1.py end to end in its harness (Table 4) and shows whether one agent already proves Lemma 2 (§2.8).
Isolate. Each run executes inside a macOS sandbox profile (sandbox-exec -f exp1.sb), in /Users/Shared/exp1/run/, holding only the inputs and the skill, in its own local session: Claude Code (claude -p) or Codex (codex exec), one harness for a whole set of 14 runs (Table 4). The kernel refuses it the repository and every earlier run, and lets it reach the web only through a proxy that refuses our own site (§2.4).
Run. Prompt 1 with $(N,v)$ filled in, one run at a time: the solve-maths skill with two rounds, the same agents and a budget of 100M tokens.
Stop at the budget. The skill's budget.py stops new rounds near 80M and the agents at 90M; run_exp1.py ends the session at 100M (Appendix A).
File. After the session ends, move the record to runs/<run>/ and the transcripts, scratch folder, token log and timings to observables/<run>/, empty the run folder, and run check_record.py (§2.5).
Check independence. Scan each transcript for paths outside the run folder and for URLs, queries or search results in $X$; rerun any run that saw $X$ (§2.4.4).
Grade blind. Fresh reviewers (/solve-maths-audit, review stage) grade every step of the record, stripped of config, reports and agent names: $\gamma(s)$; solved is graded on the verdict's proof alone (§2.8).
Measure. From the graded records: $s(c)$, $f(c)$, the mistakes $E_{\rm self}, E_{\rm miss}, F$, and tokens.
Present. Prompt 2: /solve-maths-writeup produces the compact report, main target page with supporting results, and interactive attempt tree in pages/.

A grid. Columns: k = 1, 2, 4, 8 agents. Row verifier=off: k single solver nodes S. Row verifier=paired: k/2 two-part nodes S|V, a solver and its verifier; empty for k = 1. Every cell has rounds=2, team=same, a budget of 100M tokens and two seeds. — Seven conditions; under `paired` half of the $k$ agents are verifiers.

2.2 What varies, what is fixed

Only $N$ and $v$ vary: 7 conditions; Table 1

$$\mathcal C=\{(N,\text{off}):N\in\{1,2,4,8\}\}\ \cup\ \{(N,\text{paired}):N\in\{1,2,4\}\},\qquad |\mathcal C|=7.$$

The size has four values and $v$ two, but one agent cannot be a pair, so the grid has 7 cells, not 8.

Varied and fixed hyperparameters.
	value	why
varied	`agents=`$N$: $1,2,4,8$ (off); $1,2,4$ (paired) `verifier=`$v$: off, paired	$k=N(1+[v=\text{paired}])\in\{1,2,4,8\}$: a verifier takes a solver's place
fixed	`budget=`$10^8$ tokens per run, so $B/k$ per agent `rounds=2`: round 2 is where a report is used (§2.7) `team=same`: the same $k$ agents in both rounds Prompt 1, verbatim; the portfolio chosen by the run's root at Fix harness $h$ and model per set of 14, never mixed: `cx` = Codex, `gpt-6.1-sol`, reasoning high (the first set); `cc` = Claude Code, `claude-opus-5-5`, effort high (Table 4) one frozen copy of /solve-maths (`skill.sha256`) and its templates sources: the inputs and the web, except our site $X$ (§2.4.3) grader blind to $c$ for solved, not for every step (§2.8)	runs differ only in $(N,v)$: equal total cost, the same statement, criterion and checklist; a portfolio from us would suggest the route

2.3 Seeds

What a seed is; the run order

A seed $j\in\{1,2\}$ labels a replicate. Neither Codex nor Claude Code exposes a sampling seed, so two runs of one condition differ only through the model's sampling, and no run can be reproduced. The seed fixes three things:

$$\text{run } r_{c,j}:\quad \text{name } \texttt{exp1-}\{h\}\texttt{-N}\{N\}\texttt{-}\{v\}\texttt{-s}\{j\},\qquad \text{its own directory},\qquad \text{its place in the order } \pi=\text{shuffle}_{\,\text{seed }1}(\mathcal C\times\{1,2\}).$$

The order is shuffled so that a change in the model or its load during the day does not line up with one condition. Runs share the model, the prompt and the inputs; that sharing is what makes them replicates.

2.4 Independence: what a run can read

An agent session on this Mac runs as you and, unless confined, can open whatever you can: the records and verdicts of earlier runs, your memories and session histories, CLAUDE.md and AGENTS.md, and this site, which states the lemma, the design and the checklist. A later run could then start from an earlier run's verdict, and the 14 runs would not be 14 independent tries. Isolation gives every run the same starting point, a fresh copy of the inputs and the skill, and nothing written since (Figure 2); Figure 4 shows one run from reset to filing.

Two rows of runs r_1 to r_14. Top, without isolation: every run can open all your files: earlier records and verdicts in runs/, memories and session histories in ~/.claude and ~/.codex, CLAUDE.md and AGENTS.md, and the site cwlin4916.github.io; red arcs go from each run to later runs, so two seeds of one condition are not two independent tries. Bottom, with isolation: every run starts in a fresh sandboxed folder /Users/Shared/exp1/run/ holding a checksummed copy of the inputs and a frozen copy of the skill, and reads the web except X; no arrows between runs. Formula: reads(r) is contained in D_r union (Web minus X), and reads(r) meets writes(r\') in the empty set. — Without isolation a run can read earlier runs; with it, every run starts from the same inputs.

2.4.1 Definition

Run $r$ is independent if nothing it reads was written by another run, by us after the inputs were fixed, or by an earlier session. With $D_r$ its folder /Users/Shared/exp1/run/ while it runs and $X$ our part of the web (§2.4.3):

$$\operatorname{reads}(r)\subseteq D_r\ \cup\ \text{system files}\ \cup\ (\text{Web}\setminus X),\qquad \operatorname{reads}(r)\cap\operatorname{writes}(r')=\varnothing\quad(r'\ne r).$$

A sandbox flag cannot enforce this: Codex's workspace-write limits writes, not reads, so a run handed the repository could open case-study-2-Whittaker-Category/experiment-1/runs/ and read an earlier run. Runs are therefore never handed the repository, and the kernel refuses the reads: a Seatbelt profile, applied with sandbox-exec, needs no second account and no administrator password.

$Left, the sandbox exp1.sb: one session at a time, run as you; /Users/Shared/exp1/run/ holds the current run (inputs and skill copied in, the record it writes); a carve-out of ~/.claude holds the keychain login and this session\'s own transcript and scratch folder, with no CLAUDE.md, memory, skill, plugin or other session. Right, your files, outside the profile: the experiment folder with inputs/, pages/, runs/<run>/ and observables/<run>/, and your own sessions and memories. Arrows: inputs copied in before the run; the record filed after it ends; any read from the sandbox into your files fails with Operation not permitted. Below: all traffic goes to a proxy at 127.0.0.1:8899, run outside the sandbox, which refuses hosts in X and logs the rest.$

A run sees its own folder and the open web; earlier runs and our site are out of its reach.

One run in time, three lanes. Lane run_exp1.py, as you: 1 reset (empty the run folder and its scratch), 2 copy in (inputs/ and skill/, sha256 checked), then a budget watch every 60 s (tokens.jsonl; stop at 80M, halt at 90M, end the session at 100M), then 5 file, 6 scan, 7 check (check_record.py on A_r, O_r, L_r), and a dashed arrow back to step 1 for the next run in the order pi. Lane the session, in the sandbox: 3 preflight (reads of your files denied, X refused, arXiv answers; if a check fails the run does not start), 4 run Prompt 1 (claude -p or codex exec; writes only run/). Lane proxy: every host goes to net.log, X is refused, other routes are refused by the sandbox. A host, URL, query or search result in X sends the run to runs/_discarded/ and it is rerun. — One run in time: what runs outside the sandbox, what runs inside it, and where a run is stopped or discarded.

2.4.2 Files

A sandbox profile, one run at a time, no memory or instructions

Sandbox. Every run executes under sandbox-exec -f exp1.sb, written per run into observables/<run>/. The profile denies every read and write under your home, /Users/Shared, /private/tmp, your TMPDIR and /Volumes, then allows back only the run folder, the session's scratch folder under /tmp/claude-<uid>/, the keychain (for the login) and ~/.claude minus CLAUDE.md, settings, skills, plugins, agents, commands, projects, file-history and session-env, plus this session's own transcript folder and history (by --session-id). Later rules override earlier ones, so the carve-outs are exact. Children inherit the profile: every agent, shell and script of the run is confined.
One run at a time. /Users/Shared/exp1/run/ holds only the current run: the inputs (checked against inputs.sha256), the skill (checked against skill.sha256) and what the run writes or downloads. When the session ends, the record, transcripts, scratch folder and downloads are moved into the repository and the folder is deleted. The next run starts from nothing: no earlier record, session, transcript, download or memory.
No memory, no instructions. Claude Code: --setting-sources project and --strict-mcp-config load no user settings, MCP server or connector; CLAUDE.md, user skills and memories are unreadable under the profile, and the run's auto-memory folder is moved out with its transcripts. A clean environment (env -i: home, path, proxy, auto-update off) keeps this session's variables out. Codex: a fresh CODEX_HOME inside the run folder holding a copy of auth.json; --ignore-user-config --ignore-rules; apps, plugins, browser and computer use off.

2.4.3 Internet

The web is open except our own site $X$; every route out has a guard (Table 2)

A run may search, read and download as a mathematician would: arXiv, journals, books, code, saved into $D_r$. Excluded is what is ours and public:

$$X=\{\text{the host } \texttt{cwlin4916.github.io}\}\ \cup\ \{\text{any URL or search query containing } \texttt{cwlin4916}\}.$$

$X$ covers the published site (this page and the case studies) and its copies in search caches and web archives. The repository itself is private, and the run has no GitHub login (the keychain carve-out holds only the Claude Code login).

Every way out of the runner account passes one guard.
route	where it runs	guard
shell: `curl`, `pip`, scripts	this Mac	the profile allows outbound connections only to the proxy; the proxy refuses $X$ and logs each host to `net.log`
Claude Code `WebFetch`	this Mac	the proxy, and `WebFetch(domain:cwlin4916.github.io)` denied
connectors, apps, browser, computer use	the provider; this Mac's screen	off (Prompt 1's flags); the pilot's event stream lists no MCP server and no app tool
Codex `web_search`, Claude `WebSearch`	the provider's servers	no local filter: nothing from the experiment is published until all 14 runs are filed (`experiment-1/` stays out of `gh-pages`); the scan after reads every query and every search result

; exp1.sb (excerpt), written per run by run_exp1.py; the last matching rule wins
(version 1) (allow default)
(deny network-outbound)
(allow network-outbound (remote ip "localhost:8899") (remote unix-socket))
(deny file-read* file-write* (subpath "/Users/miltonlin") (subpath "/Users/Shared") (subpath "/private/tmp") …)
(allow file-read* file-write* (subpath "/Users/Shared/exp1") (subpath "/private/tmp/claude-501/-Users-Shared-exp1-run"))
(allow file-read* file-write* (subpath "/Users/miltonlin/.claude") …)            ; login and state
(deny  file-read* file-write* (subpath "/Users/miltonlin/.claude/projects") …)   ; CLAUDE.md, skills, other sessions
(allow file-read* file-write* (subpath "/Users/miltonlin/.claude/projects/-Users-Shared-exp1-run") …)

Exercises on permissions, proxies and rule order: Exercises: isolation (written for the earlier second-account design; the rule-order exercise applies to the profile).

2.4.4 Checks

Before: the preflight must be denied; after: a scan of every read, URL and host

Before. run_exp1.py runs a preflight inside the profile, twelve checks. Listing the repository, the experiment folder, ~/.claude/projects, ~/.claude/skills, ~/.codex and /private/tmp, and reading ~/.claude/CLAUDE.md, must each fail with “Operation not permitted”. A direct connection to example.com must fail. Through the proxy, arxiv.org must answer and cwlin4916.github.io must be refused. The run folder must be writable, and the harness's CLI must start (--version, recorded in meta.json). Both skill copies and the inputs must match their checksums. Otherwise the run does not start. The output goes to observables/<run>/preflight.txt.
After. run_exp1.py lists every path a tool named outside the run folder and every URL and search query (reads.txt, web.txt), beside the proxy's net.log, and searches every tool result for cwlin4916. The profile makes a read outside $D_r$ fail, so such a path is an attempt, recorded but harmless. A run whose query, fetched URL or search result is in $X$ is moved to runs/_discarded/ and rerun under the same label.

2.5 Documenting a run

$$\operatorname{doc}(r)=(A_r,\ O_r,\ L_r):\qquad A_r=\text{what the run wrote},\quad O_r=\text{what we recorded about it},\quad L_r=\text{its line in the run list}.$$

One directory per experiment in the paper's case study, written only by run_exp1.py (filing) and Prompt 2 (pages):

case-study-2-Whittaker-Category/experiment-1/
  README.md              the run list: one line L_r per run
  inputs/                the one input folder, copied into every run: problem.md,
                         paper-excerpt.tex + preamble.tex, Zhu §1 (pdf, txt); inputs.sha256
  skill/                 the frozen /solve-maths and the one file it cites outside itself
                         (explain-math-html/references/output-style.md); skill.sha256
  scripts/               run_exp1.py, netproxy.py, check_record.py, grade_run.py, prompt1.txt
  runs/<run>/            A_r: tree.json, verdict.md, README, briefs/, returns/,
                         reports/, scripts/, STOP; audit/ (the grades γ) after grading
  runs/_discarded/       runs that failed a check, kept for the record
  observables/<run>/     O_r (Table 3)
  observables/results.json   one row per run: the inputs to Figures 5–7
  pages/                 html only: index.html (links back here), <run>.html per solved run

Artifacts are what a run wrote. Observables are what we recorded about it.
file in `observables/<run>/`	holds	used for
`prompt.txt`	Prompt 1 and the command line exactly as sent, $(N,v)$ filled in	what the run was asked
`meta.json`	label, $c$, $j$, place in $\pi$; harness, model, CLI version; start, end, exit code; last stage; $k_2$; reruns	run list; stage; rerun rule
`tokens.jsonl`	one line per `budget.py` check: time, $u$, tokens per agent, stage	Figure 7; the stop lines
`transcripts/`, `events.jsonl`	the root's and every agent's session, raw (Table 4); the CLI's event stream	tokens; reads; `wait_agent` times
`reads.txt`, `web.txt`, `net.log`	every path read; every URL and query; every host through the proxy	independence
`exp1.sb`, `preflight.txt`	the run's sandbox profile; the twelve checks before the run	independence
`scratchpad/`, `tmp/`, `workdir/`	the session's scratch folder (`STOP`); its `TMPDIR` (agents' node files, downloads); anything else the run left outside its record	halt returns; the web check of §2.8

check_record.py runs after filing; a run is documented when all three hold:

$A_r$, the record. tree.json in the skill's schema: every step has id, agent, round, time, kind, status and parents, and every step that judges earlier steps names them with an outcome in "on" (Prompt 1, Record). briefs/, returns/, reports/ verbatim, one file per agent and round. verdict.md lists $\operatorname{supp}(v^\ast)$.
$O_r$, the observables. Every file of Table 3, a transcript for the root and for every agent, and a last line of tokens.jsonl that agrees with the last stage in meta.json.
$L_r$, the run list. Label, place in $\pi$, start, end, last stage, verdict, tokens, status (filed · graded · discarded) and every rerun with its reason.

A gap in $O_r$ or $L_r$ is ours: refile, or rerun under the same label. A gap in $A_r$ is the run's: it is kept and counted, since a record that cannot be graded is itself an outcome. The grader reads runs/<run>/ only, without tree.json's "config" and reports; observables stay out of grading, since they name the condition.

2.6 Prompts

Each run starts non-interactively, so /solve-maths takes the given design without stopping to show it.

Prompt 1 (run, once per $r_{c,j}$) and Prompt 2 (write-up, once after grading)

Prompt 1 · run. For run exp1-{h}-N{N}-{v}-s{j}, run_exp1.py --harness {h} recreates /Users/Shared/exp1/run/ empty, copies inputs/ into it and the frozen skill into both run/.agents/skills/solve-maths/ (read by Codex) and run/.claude/skills/solve-maths/ (read by Claude Code), byte for byte, runs the preflight, saves the prompt and command line to observables/<run>/prompt.txt, and launches the session there inside the profile.

# SB = sandbox-exec -f observables/<run>/exp1.sb env -i HOME=… PATH=… TMPDIR=/Users/Shared/exp1/tmp/
# P  = HTTPS_PROXY=http://127.0.0.1:8899 HTTP_PROXY=…: the profile lets the run reach nothing else
# h = cx, Codex (run_exp1.py: not yet implemented); CODEX_HOME = run/.codex-run/ holding a copy of auth.json
SB P CODEX_HOME=<home> codex exec "<Prompt 1>" \
    --json --skip-git-repo-check --ignore-user-config --ignore-rules \
    -m gpt-6.1-sol -c model_reasoning_effort="high" -c web_search="live" \
    -s workspace-write -c sandbox_workspace_write.network_access=true \
    --enable multi_agent --disable apps --disable plugins \
    --disable browser_use --disable computer_use  > observables/<run>/events.jsonl
# h = cc, Claude Code; logged in through the keychain carve-out
SB P DISABLE_AUTOUPDATER=1 DISABLE_TELEMETRY=1 CLAUDE_CODE_PRINT_BG_WAIT_CEILING_MS=0 \
    claude -p "<Prompt 1>" --model claude-opus-5-5 --effort high --session-id <uuid> \
    --setting-sources project --strict-mcp-config --permission-mode bypassPermissions \
    --disallowedTools "WebFetch(domain:cwlin4916.github.io)" \
    --output-format stream-json --verbose  > observables/<run>/events.jsonl

$solve-maths agents=N rounds=2 verifier=v team=same budget=100M     Prompt 1 (h = cc: /solve-maths)

Problem.     Definition 1 and Lemma 2, pasted verbatim from this page.
Files.       inputs/: paper §2.1–2.4 (coefficients, groups, loops) and §7.1 up to
             Lemma 7.2, with its proof removed; Zhu, arXiv:1407.8519, §1.
Web.         allowed: search, read and download what helps, into this folder.
Criterion.   A complete solution proves Lemma 2 for every split reductive G over O
             and every 0 < n < ∞, as an isomorphism of functors on perfect
             F_q-algebras. Does not count: an argument on points over a field only;
             the case n = 0 (false: I̊_0 = L⁺G).
Checklist.   points vs functors on perfect algebras · T vs T_ad (t_n lies in T_ad(F)) ·
             W_O(R) vs R[[t]] · the hypotheses of any cited factorization.
Portfolio.   choose the N approach families yourself at Fix; none are suggested.
Fix.         use Problem, Criterion and Checklist verbatim.
Record.      the folder of references/repository.md: tree.json, verdict.md, briefs/,
             returns/, reports/, scripts/, every brief, return and report verbatim.
             One addition: a step that judges earlier steps, yours or another agent's,
             names them with an outcome, "on": {"A3-7": "fails"}, the outcome one of
             holds · fails · repaired. Every brief passes this rule on. verdict.md
             lists the steps the verdict uses.
Pages.       none: pages come from Prompt 2, after grading.

Prompt 2 · write-up. Uses /solve-maths-writeup. One new session in this repository, after the last run is filed and graded. E = ../case-study-2-Whittaker-Category/experiment-1/.

/solve-maths-writeup E
1. Preserve the filed verdicts/support; derive only independently supported
   outcomes and defined error statistics from existing grades. Missing = unavailable.
2. Regenerate the experiment's figures and compact report: equations,
   plots, tiny numbered tables, one short result line per logical block.
3. Give the target its own main statement/proof page with exact status and
   open obligations. Nest supporting results beneath it; on each, explain the
   target step it serves and the missing implication. Keep all original steps.
   Order: Definitions (objects included, each numbered item closed and green),
   lavender Hypotheses, theorem statement, numbered target argument; comfortable gaps.
   Read the recorded final/per-round proof drafts. Write connected mathematical
   inferences, not route summaries; label an unfinished target “Attempted proof —
   incomplete”. Separate original hypotheses from labeled gaps, mark dependent
   conclusions conditional, and present alternative routes separately.
   For older runs without a draft, save a dated presentation reconstruction in E,
   outside the original run; retain its recorded derivation and checking scope.
   Cite each supporting result where used. Each step explains its recorded
   attempt-tree contribution through linked nodes; keep open gaps explicit.
   Use one short overview, without duplicate support maps or route summaries.
   Marker-free disclosures and local object knowls. Embed the interactive tree/settings
   in the report when these are the primary evidence; omit duplicate displays
   and the duplicate Attempt tree subtab/sidebar item; retain direct node links.
4. Each numbered proof step nests ranked, checked source excerpts inside
   its argument at the point of use; keep source applicability and open transfers.
   Use Proof / Attempted argument / Conditional proof according to the step's status;
   the main attempted argument may start expanded for reading.
5. Art-only attempt trees: animate/step/play/speed/scrub + synchronized token
   bar + zoom/pan/full screen. Label elapsed time inside the tree box.
   Label recorded mistakes, gaps and repairs on their edges using words/color.
   Click an agent to expand recorded per-call input context and capacity.
   Missing telemetry stays unavailable; later reviews keep their actual scope.
6. Beside each tree, a numbered hyperparameter table: solvers, verifiers,
   rounds, team, agent count, token/time caps, model/effort and origins/defaults.
7. /no-ai-slop on prose only; preserve every mathematical claim, number,
   status, citation and proof step. Check desktop/phone, offline, interactions,
   source locators and original hashes; keep generators synchronized.
All output remains in E; no raw-data download links or automatic publication.
Use reader labels “Target” and “Recorded verdict”, not “Frozen target”.

What differs between the harnesses; the inputs, skill, prompt, budget and isolation do not.
	`cx`: Codex	`cc`: Claude Code
CLI run in the profile	`codex` inside ChatGPT.app, 0.163	`/opt/homebrew/bin/claude`, 2.1.308, auto-update off
model	`gpt-6.1-sol`, reasoning high	`claude-opus-5-5`, effort high
login	copy of `auth.json` in a fresh `CODEX_HOME`	your keychain item, readable through the profile
skill read from, invoked as	`run/.agents/skills/`, `$solve-maths`	`run/.claude/skills/`, `/solve-maths`
agents	`spawn_agent`, `wait_agent`, `followup_task`	Agent tool, SendMessage
`budget.py` runs	after every `wait_agent`	in the background, every 60 s
reads and writes confined by	`exp1.sb`, and Codex's own `workspace-write` inside it (untested)	`exp1.sb`
transcripts filed from	`$CODEX_HOME/sessions/`	`~/.claude/projects/-Users-Shared-exp1-run/`

Neither harness stops to ask: codex exec never asks for approval, and Claude Code runs with bypassPermissions, since auto mode's classifier could refuse a download or install that Codex would run. The profile and the proxy are the guards, not the harness (§2.4).

Round-1 briefs are the skill's templates (solve-maths/references/agent-brief.md; verifiers: verifier-brief.md), filled from Prompt 1 and the families the root chose. Round-2 briefs are written by $R$ at Review. Each holds the report on the agent's return, a task chosen from the report (not necessarily its own route), pointers to other agents' steps, and a line saying that it keeps its round-1 context and should reuse it. An idle agent gets no brief.

2.7 Rounds and agents

$$\text{run}(N,2,v,\text{same}):\ \ \text{Fix}\to\text{Solve}_1\to\text{Check}_1\to\text{Review}_1\to\text{Solve}_2\to\text{Check}_2\to\text{Review}_2\to\text{Verdict}.$$

The two values of $v$ differ only in who reads a step.
stage	`off`	`paired`
round 1	$N$ solvers, independent	$N$ pairs; $V_i$ checks each step of $S_i$ before it is cited
Review$_1$	$R$'s notes on each return (not a check)	$V_i$'s open issues
round 2	if the budget allows: the same agents, continued; each keeps its round-1 context. Update brief: repair · close gaps · redirect · take over another target · or idle
verdict	proved (unchecked)	proved only if nothing is open in its support

$M=2$: one round has no repair, and a third is left out. team=same keeps $k$ as the ceiling in both rounds (new would double it). $R$ may idle agents in round 2, so each run records $k_2\le k$, the agents that worked in round 2.

2.8 Design check

Six weak points and what the design does about each; Table 6

What could make the 14 runs uninformative.
risk	why	remedy
no power on $s$	$m=2$: $s(c)\in\{0,\tfrac12,1\}$; Wilson 95%: 0/2 → [0, 0.66], 2/2 → [0.34, 1], overlapping	$s$ is descriptive; the per-step counts of §4, over $\|S(r)\|\approx 20$–$100$ steps, carry the comparison
ceiling	if one agent proves Lemma 2, $s=1$ in every cell and (a) has no answer	the pilot first (§2.1); if it solves, keep (b) and the trees, or choose a harder lemma
grader sees $v$	a paired tree contains its verifiers' checks	grade solved on $\operatorname{supp}(v^\ast)$ alone, as one text; $\gamma$ on every step cannot be blind
$\sigma$ not in the record	in earlier trees an objection has parents but no outcome (§4)	the `"on"` field (Prompt 1, Record)
fewer solvers under paired	at equal $k$, $(N,\text{paired})$ has $k/2$ solvers	rates per step; the grid also compares at equal $N$: $(N,\text{off})$ vs $(N,\text{paired})$
the web finds a proof	a downloaded source may contain one	`web.txt`; mark solved runs whose support cites a download

3. Outcomes

(solved, wrong)

Run $r_{c,j}$ (condition $c$, seed $j\le m$), verdict $v^\ast$, support $\operatorname{supp}(v^\ast)$:

$$\begin{aligned} \text{claim}(r)&=\mathbf 1\big[\st(v^\ast)\in\{\text{proved},\ \text{proved (unchecked)}\}\big],\\ \text{solved}(r)&=\text{claim}(r)\cdot\mathbf 1\big[v^\ast\text{ proves Lemma 2 as stated, and }\gamma(s)\ne\text{error}\ \ \forall s\in\operatorname{supp}(v^\ast)\big],\\ \text{wrong}(r)&=\text{claim}(r)\,\big(1-\text{solved}(r)\big),\\ s(c)&=\tfrac1m\textstyle\sum_j\text{solved}(r_{c,j}),\qquad f(c)=\dfrac{\sum_j\text{wrong}(r_{c,j})}{\sum_j\text{claim}(r_{c,j})}. \end{aligned}$$

A run that reaches 100M has no verdict: $\text{claim}=0$. $\gamma(s)\in\{\text{correct},\text{minor},\text{error}\}$: the grade of step $s$ by fresh reviewers (/solve-maths-audit, review stage only), who see the record without its config, reports or agent names; the owner confirms each solved run and each error in a support.

Critical note. $\text{solved}$ and $\text{wrong}$ reduce a run to one bit, but what a run produces is its attempt tree $T(r)$ (tree.json), with its branches, dead ends, checks and repairs; the tree is what this experiment should study, and §4 is only the first measure read off it.

4. Mistakes in a run

(mistakes; self-claimed)

$S(r)$: every step of run $r$, agents' and root's, both rounds. A mistake is a step with $\gamma(s)=\text{error}$. It is self-claimed, $\sigma(s)=1$, if the run itself declared $s$ wrong before its verdict. With $\operatorname{on}_o(s)$ the outcome that step $o$ gives $s$ (Prompt 1, Record; under paired, $V_i$'s issues are such steps):

$$\sigma(s)=1\iff \text{the author set } \st(s)=\text{refuted, or some } \operatorname{on}_o(s) \text{ before the verdict is fails or repaired.}$$

“Some”, not “the last”: in the pilot a re-reading marked three repaired steps “holds” afterwards, which a last-outcome rule would have read as no claim.

$$E=\#\{\gamma=\text{error}\},\quad E_{\rm self}=\#\{\gamma=\text{error},\,\sigma=1\},\quad E_{\rm miss}=\#\{\gamma=\text{error},\,\sigma=0\},\quad M_{\rm self}=\#\{\gamma=\text{minor},\,\sigma=1\},\quad F=\#\{\gamma=\text{correct},\,\sigma=1\},$$ $$E^\ast=\#\{s\in\operatorname{supp}(v^\ast):\gamma(s)=\text{error}\}\quad\text{(the mistakes the verdict rests on).}$$

A self-claim is the run's word; the grade decides whether it was real.
	grader: error	grader: not error
run claims a mistake ($\sigma=1$)	$E_{\rm self}$, caught	$M_{\rm self}$ if minor; $F$, false alarm, if correct
run silent ($\sigma=0$)	$E_{\rm miss}$, missed	—

Measured from the record by scripts/grade_run.py: $\gamma$ from audit/G*.json, merged into tree.json; $\sigma$ from the "on" fields; one row per run in observables/results.json. Counts are per run, reported with $|S(r)|$, since more agents write more steps. Without a grader a reader sees only $E_{\rm self}+F$; recall $E_{\rm self}/E$ and precision $E_{\rm self}/(E_{\rm self}+F)$ say how far to trust it.

Earlier runs: self-claims are common; the one graded run caught at most 1 of its 15 errors (Table 8)

The 14 earlier /solve-maths runs, rounds 1–2; $\sigma$ read by hand from objection and check titles, since `"on"` did not exist.
runs	steps	self-claims	errors $E$	caught $E_{\rm self}$
satake-converse (graded by a fresh audit)	70	1	15	≤ 1
13 others (ungraded)	373	21, in 8 runs	—	—

Self-claims occur, mostly as round-2 objections (“step 3 fails for dim ≥ 2”, “the claim is too strong”). In satake-converse, whose round 2 was spent on audits, 7 of the 15 errors were checked there and passed, and 14 were found only by the fresh audit afterwards; (b) asks whether paired verifiers change that.

5. What to plot

(a) along the off row, $\textbf{H}_a$: $s(N,\text{off})$ non-decreasing in $N$; (b) at equal $k$, $\textbf{H}_b$: $E_{\rm miss}$ and $f$ lower under paired, with $s$ not much lower. Figures 5–7 and the run list: Results.

Earlier evidence

On the number of agents and on verifiers.
study	finding
Li et al. 2024	sampling-and-voting: accuracy rises with the number of agents, more on harder tasks
Zhang et al. 2025	debate rarely beats chain-of-thought or self-consistency, despite more compute
Kim et al. 2025	agents help on parallelizable tasks, hurt on sequential ones
Huang et al. 2024	without outside feedback, self-correction does not help
Lifshitz et al. 2025	more verifiers improve best-of-$n$, but not at small budgets
Petrov et al. 2025	full LLM proofs mostly fail under expert grading

Appendix A. Token budget

When budget.py stops a run: 80M, 90M, 100M

$u(t)$ counts the tokens of $R$ and every agent since the Fix, each model call in the transcripts as input + cache writes + cache reads + output. budget.py recomputes $u$ from the run's transcripts, after every wait_agent under Codex and every 60 s under Claude Code (run_exp1.py also checks every 60 s for the last line) (skill):

$$\begin{array}{lll} u\lt 80\text{M} & \text{go} & \text{round 2 starts only if } u+\hat c_2\le 80\text{M},\quad \hat c_2=c_1\cdot k_2/k\\ u\ge 80\text{M} & \text{stop} & \texttt{STOP}\text{ written; each agent returns at its next step; Verdict}\\ u\ge 90\text{M} & \text{halt} & R\text{ stops the agents still running and takes their node files as returns}\\ u\ge 100\text{M} & \text{over} & \texttt{run\_exp1.py}\text{ ends the session; no verdict} \end{array}$$

$c_1$: tokens of round 1; $k_2$: agents working in round 2. For scale, the worked example used 63M tokens with 9 agents over two rounds, 28M of them $R$'s own calls. Each check appends a line to observables/<run>/tokens.jsonl; the last stage goes to meta.json. A run cut off by the subscription's usage limit is discarded and rerun under the same label.

Status, 30 October 2026. Made: the inputs and inputs.sha256; the frozen skill and skill.sha256; run_exp1.py --harness cc, netproxy.py, exp1.sb, check_record.py, grade_run.py; the Claude Code pilot (run 30 October 2026; its report stays on the private branch until the 14 runs are filed). Still needed: --harness cx in run_exp1.py and the Codex pilot; figures/make_exp1_figures.py reading observables/results.json (filled by grade_run.py, made with the pilot); a first run of verifier=paired (made 29 October 2026).

	grader: error	grader: not error
run claims a mistake (\(\sigma=1\))	\(E_{\rm self}\), caught	\(M_{\rm self}\) if minor; \(F\), false alarm, if correct
run silent (\(\sigma=0\))	\(E_{\rm miss}\), missed	—

	value	why
varied	`agents=`\(N\): \(1,2,4,8\) (off); \(1,2,4\) (paired) `verifier=`\(v\): off, paired	\(k=N(1+[v=\text{paired}])\in\{1,2,4,8\}\): a verifier takes a solver's place
fixed	`budget=`\(10^8\) tokens per run, so \(B/k\) per agent `rounds=2`: round 2 is where a report is used (§2.7) `team=same`: the same \(k\) agents in both rounds Prompt 1, verbatim; the portfolio chosen by the run's root at Fix harness \(h\) and model per set of 14, never mixed: `cx` = Codex, `gpt-6.1-sol`, reasoning high (the first set); `cc` = Claude Code, `claude-opus-5-5`, effort high (Table 4) one frozen copy of /solve-maths (`skill.sha256`) and its templates sources: the inputs and the web, except our site \(X\) (§2.4.3) grader blind to \(c\) for solved, not for every step (§2.8)	runs differ only in \((N,v)\): equal total cost, the same statement, criterion and checklist; a portfolio from us would suggest the route

stage	`off`	`paired`
round 1	\(N\) solvers, independent	\(N\) pairs; \(V_i\) checks each step of \(S_i\) before it is cited
Review\(_1\)	\(R\)'s notes on each return (not a check)	\(V_i\)'s open issues
round 2	if the budget allows: the same agents, continued; each keeps its round-1 context. Update brief: repair · close gaps · redirect · take over another target · or idle
verdict	proved (unchecked)	proved only if nothing is open in its support

risk	why	remedy
no power on \(s\)	\(m=2\): \(s(c)\in\{0,\tfrac12,1\}\); Wilson 95%: 0/2 → [0, 0.66], 2/2 → [0.34, 1], overlapping	\(s\) is descriptive; the per-step counts of §4, over \(\|S(r)\|\approx 20\)–\(100\) steps, carry the comparison
ceiling	if one agent proves Lemma 2, \(s=1\) in every cell and (a) has no answer	the pilot first (§2.1); if it solves, keep (b) and the trees, or choose a harder lemma
grader sees \(v\)	a paired tree contains its verifiers' checks	grade solved on \(\operatorname{supp}(v^\ast)\) alone, as one text; \(\gamma\) on every step cannot be blind
\(\sigma\) not in the record	in earlier trees an objection has parents but no outcome (§4)	the `"on"` field (Prompt 1, Record)
fewer solvers under paired	at equal \(k\), \((N,\text{paired})\) has \(k/2\) solvers	rates per step; the grid also compares at equal \(N\): \((N,\text{off})\) vs \((N,\text{paired})\)
the web finds a proof	a downloaded source may contain one	`web.txt`; mark solved runs whose support cites a download