/proof-derivation-forensics

name: proof-derivation-forensics
description: "Family-G proof & derivation integrity forensics: does a THIRD PARTY's written proof/derivation actually establish its theorem, or does it skip an obligation, assume its own conclusion, take an invalid step, drift a symbol's meaning, or smuggle an unstated assumption? Decides from the WRITTEN proof/derivation — verdict-bearing at L1 (the LaTeX source; PDF-extracted math is unreliable, so an L0 PDF-only run surfaces info only) — never asserts 'fabricated', only that the step shown does not hold. A fresh cross-model reviewer reads the theorem/proof + an extraction-only obligation scaffold and proposes per-obligation findings, each span-anchored to the evidence ledger (claims.json); reviewer≠adjudicator. Emits proof-derivation-forensics.findings.json; NEVER computes the verdict. dimension=proof, can be critical. Triggers: \"proof forensics\", \"check this proof\", \"derivation integrity\", \"audit the math\", \"证明审计\", \"推导有没有漏洞\"."
argument-hint: [paper-dir | claims.json]
allowed-tools: Bash(*), Read, Write, mcp__codex__codex

Proof & Derivation Forensics — does the written proof hold?

Audit family **G (proof & derivation integrity)** for: **$ARGUMENTS** (requires `claims.json` from `/evidence-ledger`). A fresh cross-model reviewer reads each theorem/proof and proposes span-anchored findings; this skill writes `proof-derivation-forensics.findings.json`. The deterministic adjudicator — not this skill — computes the verdict.

> 🔒 **Do not wrap this skill in `/loop`, `/schedule`, or `CronCreate`.** It is > verdict-bearing input — it proposes the findings the deterministic adjudicator > turns into the report. Re-firing it on a wall-clock timer adds no signal: its > output changes only when the **paper / ledger** changes, not with the clock. > Schedule the *external wait that precedes it* — ledger built → audit **once**. > (Mirrors ARIS's external-cadence doctrine.)

> Broken math is the single most-cited "obviously machine-written" tell in real > reviews ("过不去的步骤用文字糊弄", "车轱辘话复述当证明", "关键公式符号用反"). Unlike the > surface signals of family F, family-G flaws are **substantive** and **can be > critical**: a theorem whose proof is circular, skips a load-bearing obligation, or > takes an invalid step **does not support its claim**. And — crucially — proof > validity is decidable from the *written* proof: we never need the code or results, > so family G is **verdict-bearing at L1** (the LaTeX source) and can still reach > HARD_FLAGS with no repo — but needs that source, because PDF-extracted math is > unreliable; at an L0 (PDF-only) run a family-G flaw surfaces as `info` only. Adapted from ARIS > `proof-checker` (per-obligation ledger + 20-category taxonomy + counterexample red > team) and `formula-derivation` (identity/proposition/approximation/interpretation > step typing), **reframed from "fix my own proof" to "audit a third party's proof, > detect-only."** There is no fixing here and no authorship verdict — only "the step > shown does not hold," with the exact line quoted.

Why this exists

An autoresearch pipeline (or a rushed human) writes a theorem statement, then a proof, then an abstract that advertises the theorem — in separate passes, never reconciled at the level of the *argument*. The result is a proof that does not establish its own claim:

• "By compactness a maximizer exists" — but compactness of the domain is never shown

(a missing existence obligation invoked as fact);

• "Lemma 3 follows from Theorem 1," whose proof in turn invokes Lemma 3 (circular);
• "By Jensen, $\mathbb{E}[f(X)] \ge f(\mathbb{E}[X])$" for a **concave** $f$ — the

inequality runs the wrong way (an invalid step);

• the definition fixes $\le$, but equation (7) and the proof use $\ge$; or `argmin`

in Def 2 becomes `argmax` in the proof of Thm 4 (a symbol's meaning drifts);

• a concentration bound uses **independence** of the $X_i$, but the theorem only

assumes they are identically distributed (a stronger assumption smuggled in).

None of this needs the code, the data, or any external fact to detect — only the proof, read against the obligations its own theorem creates. That is why family G is **substantive and decided from the written proof (verdict-bearing at L1)**: a senior area chair reads a proof and decides validity from the page; this tool needs the LaTeX source (L1) to do it reliably, since PDF-extracted math is unreliable — at an L0 PDF-only run it surfaces info only. So does this skill — via a cross-model reviewer, with every finding anchored to a verbatim ledger span and the verdict computed by deterministic code.

**Honest recall bound (read this).** The evidence ledger (`build_claim_ledger.py`) has **no dedicated theorem/proof/equation extractor**: proof text enters `claims.json` only as the `number`, `scope`, `citation`, `caption`, and `table_cell` spans that happen to *overlap* it (a bound with a constant, a "for all / general" sentence, a `\cite{}` to an imported result, an equation paragraph carrying a decimal). The reviewer **judges from the full proof source**, but every finding must **anchor to a ledger claim** whose `text_span` verbatim-contains the failing fragment. A pure-symbol step covered by no such claim cannot rise above `info` — that is the honest outcome, not a defect. Recall is materially higher at **L1** (LaTeX: equation paragraphs and theorem-statement sentences are captured with stable line numbers) than at **L0** (PDF text). Step 1 pre-computes, per theorem, the exact **anchor-candidate** `claim_id`s so the reviewer knows where it can and cannot ground a finding.

Core principle

**Ledger-anchored, span-verified, decide-from-the-written-proof, reviewer≠adjudicator.** There is **no deterministic tool** for family G (no arithmetic backbone like consistency-audit's `check_numeric_consistency.py`) — proof validity is a semantic judgment. So this skill runs exactly one substantive pass:

• a **fresh cross-model** reviewer