Multiagent with verifier · verifier=paired

Every solver with a weak verifier

The verifier=paired option of /solve-maths (made): root $R$ plus $N\le 4$ pairs $(S_i,V_i)$. The verifier $V_i$ does not certify a step: it runs named checks and reports issues anyone can check. Only issues block; an approval certifies nothing.

Why: errors stayed in the record for hours

Fifteen errors of the satake-two-levels run: five found by auditor A7 within 16 to 50 minutes, ten found only after the run, 120 to 216 minutes after they were written — Two thirds of the errors were found only after the run ended; by then up to 6 later steps cited each one.

Errors in the worked example's 110 steps.
found	errors
inside the run, by auditor A7 (median 33 min after writing)	5
only after the run, by fresh reviewers (median 175 min)	10

Can a verifier grade a research step?

Not as “correct”. Without an answer key, an LLM's approval is weak evidence:

LLM verdicts on proofs without a reference solution.
source	setting	result
[Mahdavi et al., Table 3]	olympiad proofs	o1 labels 31 % of correct and 39 % of fallacious solutions “correct”
[Ma et al., Table 1]	olympiad proofs, 0–7 scale	o3: error 0.96 with a reference, 1.68 without, biased +0.92 upward
[Pandit et al., Fig. 4]	step-level, frontier maths	weaker verifiers fail by calling every step correct
[Feng, Trinh et al., Table 6]	Erdős problems	212 answers passed the verifier; of 200 decided by experts, 31.5 % correct, 6.5 % meaningfully
worked example	Satake, two levels	in-run auditor found 5 of 15 errors; 3 more were in its own steps

But a reported issue with a location and a reason is checkable in one step, and checking an issue is easier than finding one [Shao et al., §2.1.2]. So the verifier's job is reversed:

$$\underbrace{V(s)\in\{\text{correct},\text{minor},\text{error}\}}_{\text{strict: certify}}\qquad\longrightarrow\qquad \underbrace{V(s)=\big(K(s),\,I(s)\big)}_{\text{weak: checks run, issues found}}$$

What to check: the errors we had

The 15 errors of the worked example, by the check whose scope contains them (classified from the reviewers' findings).
check	$V_i$ does	evidence it leaves	errors
scope	matches every cited result's hypotheses and setting (field, characteristic, (A1)–(A5)) to the step's	quoted hypothesis + result number	7
compute	evaluates the claim in the smallest case: $q=2,3$; $\mathrm{GL}_4$; $m=2$	a script	6
depend	checks that no parent has an open issue	parent ids	1
logic	re-derives the inference; looks for circularity	the re-derivation	1

scope: A3-11, A7-16, A5-8, A7-24, A8-10, R-1, R-4 · compute: A4-10, A1-4, A5-6, A1-2, A8-5, A7-11 · depend: A1-9 · logic: A4-11. “In scope” is not “would have been caught”: that is the test.

Result: 14 of 15 errors fall under checks that leave mechanical evidence; only one needed reading the logic.

The report and the gate

(verifier report)

$$V_i(s)=\big(K(s),\,I(s)\big),\qquad K(s)\subseteq\{\text{scope},\text{compute},\text{depend},\text{logic}\},\qquad \iota=(\mathrm{sev},\ \mathrm{loc},\ \mathrm{reason},\ \mathrm{evidence})\in I(s),$$

$\mathrm{sev}(\iota)\in\{\text{critical},\text{gap}\}$: a critical issue breaks the step; for a gap the verifier assumes the claim and continues [Huang & Yang, §2.3]. A step too large to check gets the gap “split”.

(life of an issue)

$$\text{open}\ \longrightarrow\ \begin{cases}\text{resolved} & S_i \text{ repairs } s,\ V_i \text{ re-checks},\\[2pt] \text{dismissed} & S_i \text{ disputes},\ V_j\ (j\ne i) \text{ finds the issue not real}.\end{cases}$$

$\open(s)$ = the open issues of $s$; $\open_{\mathrm{crit}}(s)$ the critical ones.

(gate)

$$\begin{aligned} &\textbf{cite: } && s\to s'\ \Rightarrow\ t\big(V(s)\big)\le t(s')\ \text{and}\ \open_{\mathrm{crit}}(s)=\varnothing,\\ &\textbf{carry: } && \text{the gaps of } s \text{ are listed on every } s' \text{ with } s\in\supp(s'),\\ &\textbf{verdict: } && \st(v^\ast)=\text{proved}\ \Rightarrow\ \open(u)=\varnothing\ \ \forall\,u\in\supp(v^\ast);\\ & && \text{otherwise } \st(v^\ast)=\text{partial, with } \textstyle\bigcup_{u}\open(u) \text{ as its obligations.} \end{aligned}$$

The verifier can block a step (with a reason) or lower a status; it never raises one. A critical error lives at most $t(V(s))-t(s)$, not until the run's end ().

Architecture

Teal: proof work; violet: checks; blue: the root; dashed: a disputed issue goes to another pair's verifier. The process audit is a script, not an agent.

Flow

Problem + references
├── Fix          statement, setting, completion criterion, checklist
├── Portfolio    N ≤ 4 approaches → pairs (S_i, V_i)    2N ≤ 9 agents
├── Round 1      in each pair, in parallel:
│     S_i writes step s ──► V_i: scope → depend → compute → logic ──► report
│     critical issue? S_i repairs (V_i re-checks) or disputes (V_j decides)
├── Registry     R lists citable steps and open gaps; check_invariants.py: I1–I8
├── Rounds 2…M   update briefs: repairs, redirects; team=same keeps the pairs
├── Verdict      proved / partial with obligations
└── Record       as /solve-maths, plus every report

Who does what

Each role sees only what it needs.
role	sees	does	never
solver $S_i$	its brief; its reports	writes one inference per step, each citation with result number and quoted hypotheses	cites a step with an open critical issue
verifier $V_i$	the setting; one step with its parents' statements and the sources	runs the four checks, cheapest first; reports issues with evidence	certifies, repairs, or sees the solver's notes
root $R$	steps, reports, script output	registry, dispute routing, verdict	raises a status a report lowered
`check_invariants.py`	the record	tests I1–I8	judges the mathematics

What a pair exchanges

Step · S → V

{"id": "S2-4", "t": "…Z",
 "statement": "…",
 "parents": [{"id": "S2-1",
   "statement": "…"}],
 "cites": [{"src": "…, Prop. 41",
   "hyp": "G split, p odd"}],
 "body": "one inference"}

→

Report · V → S, R

{"step": "S2-4", "t": "…Z",
 "ran": ["scope", "depend",
         "compute"],
 "issues": [{"sev": "critical",
   "loc": "line 2",
   "reason": "Prop. 41 needs
              p odd; here p = 2",
   "evidence": "quote, p. 12"}]}

dispute →

Meta-check · V_j → R

{"issue": "S2-4#1",
 "real": true,
 "reason": "p = 2 allowed
   by the Fix's setting"}

Invariants the pairs add

I1–I6 are defined on the audit page.

$$\textbf{I7 gate: }\ t(s)\le t\big(V(s)\big)\le \min_{s\to c}\, t(c),\qquad \textbf{I8 evidence: }\ \forall\,\iota\in I(s)\ \forall\,k\in K(s):\ \text{a quote, script or id is attached}.$$

Budget

$$\#\text{agents}=2N\cdot\begin{cases}1 & \texttt{team=same}\\ M & \texttt{team=new}\end{cases}\ \le 9\ \Rightarrow\ N\le 4,$$

the budget of every /solve-maths option (run); cost per pair $C_S+C_V$, with $C_V<C_S$ when the logic check is spent only where the cheaper checks leave doubt.

Design choices

Report, not grade. Without a key, LLM verdicts on proofs are lenient or near random (); an issue with a location can be checked by anyone [Huang & Yang].
Checks from our errors. Scope and compute cover 13 of 15 (); misquoted results are the subtle failure of research agents with search [Feng, Trinh et al., §2.3]; debate works only with verified quotes [Khan et al., §2.2].
Meta-check disputes. Verifiers trained on scores alone invent issues; checking an issue is easier [Shao et al., §2.1.2]; LLM critics trade recall for hallucinated bugs [McAleese et al., §3.4]. A false critical costs one meta-check, not a lost step.
Small steps. A weak verifier is meaningful when the prover writes checkably [Kirchner et al., Anil et al.]; a dispute narrows to one step [Irving et al., §2.2].
Depth, not votes. On step-level checking, longer reasoning helps and majority voting does not [Pandit et al., §4.4]; vary the strategy across $V_1,\dots,V_4$ instead [MAV, Table 4].
Process by script. The per-unit auditor only checked invariants of the record, so check_invariants.py does it; $N$ falls from 13 to 9.
Harness clock. $t(s)$ is the harness's timestamp, so I3 and I7 can be enforced [Lamport].
A filter, not a certifier. on Erdős problems the verifier pre-filtered for human review [Feng et al.].

Test before use

$$\mathrm{recall}_c(V)=\frac{\#\{\text{errors in scope of check } c \text{ that } V \text{ reports critical}\}}{\#\{\text{errors in scope of } c\}},\qquad \mathrm{false\ critical}(V)=\frac{\#\{\text{correct steps reported critical}\}}{\#\{\text{correct steps shown}\}}$$

on the 15 errors of and as many steps graded correct (verifying agent).

Files the option would add

.claude/skills/solve-maths/        (mirrored in .agents/skills/)
  SKILL.md                 verifier=paired: pairs → gate → verdict
  references/
    agent-brief.md         + one inference per step, quoted hypotheses for every citation
    verifier-brief.md      four checks, cheapest first · report schema      (new)
  scripts/
    check_invariants.py    I1–I8 (new; I7–I8 under paired)

Status: made, 29 October 2026 (Skill changes); not yet run. The skill's check_invariants.py reads tree.json; the older copy here reads data.json.

role	sees	does	never
solver \(S_i\)	its brief; its reports	writes one inference per step, each citation with result number and quoted hypotheses	cites a step with an open critical issue
verifier \(V_i\)	the setting; one step with its parents' statements and the sources	runs the four checks, cheapest first; reports issues with evidence	certifies, repairs, or sees the solver's notes
root \(R\)	steps, reports, script output	registry, dispute routing, verdict	raises a status a report lowered
`check_invariants.py`	the record	tests I1–I8	judges the mathematics