verify-math

name	verify-math
description	Verify a self-authored mathematical result end to end by routing claims across adversarial review, numerical falsification, symbolic or CAS checks, and Lean, then aggregating one report. Use when a theorem, proposition, conjecture, or paper-wide mathematical argument needs the appropriate combination of verification methods. For one known method, use $numerical-check, $symbolic-check, or $lean-check directly.
allowed-tools	["Read","Grep","Bash","AskUserQuestion","Skill","Task","Write","Edit"]
agent-dependencies	["domain-reviewer"]

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)
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.

When the claim lives in LaTeX, extract a self-contained theorem/proof block before dispatch:

uv run python <skill-dir>/scripts/extract_block.py paper/sections/model.tex "prop:concavity"

The helper includes an immediately following proof and any displayed equations referenced by label. Inspect the output and add missing definitions or assumptions before giving it to a reviewer or computational rung.

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-routing mechanism (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).

For a hard proof strategy, existence/uniqueness question, or counterexample search that resists the standard rungs, use an adversarial reasoning pass as lead generation, never as a verdict. Make the prompt self-contained: state the exact claim, define every symbol and parameter domain, describe failed approaches, request multiple concrete strategies, and demand explicit algebra or numerical counterexamples. Route every proposed proof step or counterexample back through R1, R2, R3, or the fresh-context R0 reviewer before relying on it.

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.
• Don't treat a persuasive exploratory proof or counterexample as verification — it remains a lead until a verification rung checks it.

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.