verify-math

name	verify-math
description	Use when you need to VERIFY a self-authored mathematical result end-to-end — route each claim to the right rung of the verification spectrum (R0 adversarial review, R1 numerical falsification, R2 symbolic/CAS, R3 Lean proof) and aggregate into one verification report. The umbrella over /numerical-check, /symbolic-check, /lean-check, and the domain-reviewer agent. Triggers: /verify-math, 'verify this theorem/proposition/conjecture', 'check all the math in my paper', 'is this result correct'. Use when you have a claim and want the right method(s) chosen and combined; for a single known method, call that skill directly.
allowed-tools	["Read","Grep","Bash","AskUserQuestion","Skill","Task","Write","Edit"]

Verify Math: Route a Math Claim Through the Verification Spectrum

The front door for verifying self-authored mathematics. Classify each claim, dispatch it to the strongest applicable rung(s), and merge the sub-verdicts into one report. This skill does not verify anything itself — it routes and aggregates; the rungs do the work.

When to Use

• You have a Proposition / Theorem / Conjecture (or a whole paper's worth) and want it verified with the right method(s), possibly combined.
• /verify-math, "verify this theorem", "check all the math in the paper", "is this result correct".
• The operational front end of mark-unverified: run this before asserting a self-authored result.

When NOT to Use

• You already know the single method → call it directly (/numerical-check, /symbolic-check, /lean-check, or domain-reviewer).
• Non-mathematical claims (citations, prose) → /proofread, /bib-validate, domain-reviewer.

The verification spectrum (the rungs it routes to)

Rung	Method	Can it…	Tool
R0	adversarial deductive read	catch conceptual/assumption gaps (no proof)	domain-reviewer (agent) / codex-math
R1	numerical falsification	falsify definitively; support (never prove)	/numerical-check
R2	symbolic / CAS	prove or falsify an algebra step	/symbolic-check
R3	formal Lean proof	prove (strongest)	/lean-check

Procedure

1. Decompose the result into atomic claims

A theorem is usually several obligations. List each separately: the algebra steps, the distributional/parameter-space claims, the load-bearing lemma, the conceptual assumptions. Verify each with the rung that fits — a single "verdict" on a compound theorem hides which part is shaky.

2. Classify each claim → rung

Claim shape	Rung	Route to
algebra / derivative / limit / closed-form identity	R2	/symbolic-check
monotonicity / threshold / comparative-static / inequality over a parameter space (distributional, probabilistic)	R1	/numerical-check
a critical, faithfully-formalizable lemma	R3	/lean-check
conceptual correctness, assumption completeness, code-theory alignment	R0	domain-reviewer (Task/agent)

3. Order: falsify cheap → prove expensive

• Falsify first with the cheapest applicable rung (usually R1 numerical, or R2 for algebra). A counterexample stops the pipeline — no point proving a false claim.
• Then prove the survivors with a proving rung (R2 for algebra, R3 for the key lemma) if the claim is important enough to warrant a positive guarantee.
• R0 domain-reviewer runs across the whole result for the conceptual/assumption layer the computational rungs can't see.
• Present the routing plan (claim → rung) and, when it involves R3 (expensive) or ambiguity, confirm with the user before dispatching.

4. Dispatch

• Invoke each rung skill via the Skill tool (/numerical-check, /symbolic-check, /lean-check); dispatch domain-reviewer via the Agent tool (fresh context — it reviews math it didn't write, per agents-vs-skills).
• Each rung writes its own reviews/<scope>/verify-<method>/… report (shared shape).

5. Aggregate → one verdict

Condition	Aggregate verdict
Any rung returns FALSIFIED	FALSIFIED (name which claim + counterexample)
A proving rung (R2/R3) VERIFIES the core claim, nothing falsified	VERIFIED (note the guarantee level: CAS vs Lean)
Only R1 supports (no counterexample), no proving rung	INCONCLUSIVE (supported: no counterexample in N)
Rungs couldn't decide / not formalizable	INCONCLUSIVE
Setup/toolchain failure	ERROR

Numerical alone is never VERIFIED. Only a proving rung (R2/R3) upgrades a claim from "unfalsified" to "verified".

Anti-Patterns

• Don't collapse a compound theorem into one verdict — decompose; report per-obligation so the shaky step is visible.
• Don't report VERIFIED off R1 (numerical) alone — that's INCONCLUSIVE(supported); numerical can't prove.
• Don't prove before falsifying — a cheap counterexample saves an expensive Lean effort.
• Don't self-review the conceptual layer — dispatch domain-reviewer as a fresh-context agent (the session that wrote the math is blind to its own gaps).
• Don't skip R0 — the computational rungs verify the math as stated; they can't catch a wrong assumption or a statement that doesn't mean what you think.

Output — Aggregate Verification Report

Write to reviews/<scope>/verify-math/<YYYY-MM-DD-HHMM>.md:

result:   <the theorem/proposition being verified>
claims:   (one row per atomic obligation)
  - <claim 1> | rung R? | verdict | evidence/report link
  - <claim 2> | rung R? | verdict | ...
verdict:  VERIFIED (Lean|CAS) | FALSIFIED (<which claim>) | INCONCLUSIVE(supported|undecided) | ERROR
guarantee: <the weakest link — the result is only as verified as its least-verified obligation>
next:     <what to escalate — e.g. "obligation 3 unfalsified by R1; Lean-prove it (R3)">

Verification (did this skill work?)

• Each atomic claim has a rung + a sub-verdict + a linked sub-report.
• The aggregate verdict follows the table (FALSIFIED dominates; VERIFIED requires a proving rung).
• The guarantee line names the weakest link honestly.

Worked example — 2026-07-04 (median-collapse paper), how it would route

• Threshold ρ* = (μ_med/μ_max)² (closed-form identity) → R2 /symbolic-check → VERIFIED.
• Prop 3.1 d/dρ Φ(μ/√ρ) < 0 (derivative sign) → R2 → VERIFIED.
• "Q₀(∞;ρ) monotone in ρ for all competence" (distributional monotonicity) → R1 /numerical-check → FALSIFIED (bimodal counterexample) ⇒ aggregate FALSIFIED for that claim; conjecture removed.
• Median collapse / assumptions (conceptual) → R0 domain-reviewer → substantive check.
• Aggregate: the paper's symmetric theorem VERIFIED (CAS); the general conjecture FALSIFIED (R1) — exactly the split the paper now reports.