# Verifying Proofs

> Use when checking the mathematics of a paper rather than its claims — verifying a theorem's proof, an algebraic derivation, a bound, or an appendix full of lemmas. Triggers on "check this proof", "verify the derivation", "is Lemma 3 correct", "does the algebra work", a paper directory containing theorem/proof environments, or a referee asking whether a mathematical argument holds.

- Skill: `chgagne/verifying-proofs` (Agent Skill, multi-file: 33 files)
- Install (CLI): `npx skillmds@latest add chgagne/verifying-proofs`
- Raw SKILL.md: https://api.skillmd.com/api/skills/chgagne/verifying-proofs/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: chgagne (https://skillmd.com/u/chgagne)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/chgagne/verifying-proofs

---


# Verifying Proofs

## Overview

**A proof is refuted one step at a time, and reported one gap at a time.** The
useful output of this skill is rarely "the theorem is false" — it is *this step
needs a hypothesis nobody stated*, *this induction has no base case*, *this
lemma's appendix restatement drops a condition its proof uses*.

**Core principle: the tool may never report its own limitations as the paper's
mistakes.** Every rule below exists to keep that true. A checker that says
"counterexample at $x = -11/5$" about a step that plainly meant $x > 0$ has not
found an error; it has taught its reader to ignore the next twenty findings.

Two consequences, both measured on real papers:

- **A symbol whose domain the paper never stated can never produce a
  counterexample.** On arXiv:1509.01240, 54 of 61 symbols had no readable domain.
  Sampling those freely would have produced dozens of "errors" against correct
  mathematics.
- **The default run is a hygiene checker, not a correctness checker.** Measured
  against six papers with documented, localised proof errors, the no-CAS engines
  found **none of them**. What they do find — a dependency cycle, an induction
  with no base case, a restatement that drops a hypothesis, a division by
  something nobody proved non-zero — is worth having, and it is not the same
  thing as checking whether the mathematics is right. **To check correctness you
  must fill in check scripts**, and doing so refuted a step in Adam's convergence
  proof exactly. See *Measured results*.

## Run it

```sh
python3 ~/.claude/skills/verifying-proofs/assets/run-proofcheck.py main.tex \
    --out review-assets/
```

Run it by absolute path from the paper directory. Stdlib only — no install, no
venv, no dependencies. SymPy and Z3 are *optional external checkers*: probed at
runtime, never installed, and their absence degrades the run instead of breaking
it.

- `--engines sideconds,rational,symbolic` — default is `sideconds` alone, which
  needs nothing external and produced every finding in the measurements below.
  Every scripted engine named gets **its own script per step**
  (`checks/<step>.<engine>.py`), and engines that disagree compose to
  `UNVERIFIED` rather than to a finding
- `--claims thm:main,lem:2` — restrict to named claims
- `--emit-symbols-template` — **run this first on any real paper.** Writes a
  `--symbols` skeleton for every symbol whose domain the paper never states,
  ordered by how many unmet side conditions each one stands in, with a sidecar
  naming the obligations it blocks and the legal values
- `--symbols symbols.json` — `{"\\gamma": "unit-interval-half-open"}`; one minute
  of your time unblocks more checking than any amount of inference. A value
  outside the known vocabulary is now **refused with the nearest legal name**
  rather than accepted and silently matching nothing
- `--emit-stubs-only` — write every check script and run nothing, so you can read
  what would run first
- `--ledger-only` — write `proof-ledger.json` and stop
- `--translations A.json,B.json` — adjudicate **two independent agent-authored
  translations** of the emitted scripts. See *Two translations* below; this is the
  only route by which an agent-written `build()` may produce a `CRITICAL`
- Exit code `2` means degraded coverage — a checker was missing, a script was not
  translated, or the segmenter dropped proof text

Outputs into `--out`: `proof-ledger.json`, `proofcheck-report.md`,
`proofsteps.csv`, and `checks/*.py`.

## Two translations, when an agent writes `build()`

The default engines write their own models. When you instead have an agent fill in
`build()`, a new failure appears that no other guard covers: **a model that quietly
drops a term produces a counterexample against correct mathematics.** Reading the
round-trip display catches some of it and does not scale.

Two independent translations do. If a refutation is an artefact of how one agent
read the LaTeX, a second agent is unlikely to misread it the same way.

```sh
# 1. emit the scripts and read them
run-proofcheck.py main.tex --out ra/ --engines symbolic --emit-stubs-only

# 2. dispatch two subagents, independently, each writing build() for every step.
#    Each returns {step_id: {build, ignored_symbols, translation_confidence,
#    translation_notes}} as JSON. Do not let them share a working directory.

# 3. adjudicate
run-proofcheck.py main.tex --out ra/ --engines symbolic --translations A.json,B.json
```

**The rule: a `CRITICAL` requires both translations to refute.** One refuting and
one not is `UNVERIFIED` — not a weaker finding, for the same reason composition
rule 3 says disagreeing engines yield `UNVERIFIED`. This extends that rule from
engines to translations. Coverage is the **intersection**: a step only one
translation modelled is named in the report and folded in on nobody's vote.

Writes `two-translation-agreement.md` and `agreement.json`. **Read the agreement
rate first** — it is the false-positive control, and below about 80% the problem
is the contract, not the mathematics.

### What it costs, honestly

Two subagents per document rather than per step, each writing one `build()` per
triaged step. Measured over 10 papers and 126 steps: 20 translators, **94%
aggregate agreement**, above 80% on every paper. That is not free, and it buys one
thing — the right to report an agent-authored refutation at all.

**Give the two translators private copies of the stubs.** On the measured run they
were pointed at a shared directory and one noticed the other's edits. Independence
is the entire control; a shared working directory silently voids it.

**Prefer Z3 to SymPy for the engine you translate against.** The same 18 Adam steps
scored **28% agreement through SymPy translations and 94% through Z3 ones**, and the
cause was not translator reliability. It is that the symbol vocabulary cannot state
a bound like `\beta < 1` or `x \geq 1` — only membership in a named domain — so one
agent keeps a parameter symbolic and reaches unreachable points while the other
instantiates it at rationals and reports scale-dependent artefacts. Where the
refutation depends on a numeric bound, the symbolic engine will honestly return
`UNVERIFIED` rather than decide.

## What gets checked, and by what

```
0. side conditions + structure   stdlib      always runs, needs nothing
1. randomized exact rationals    stdlib      can refute; never confirms
2. SymPy equivalence             optional    the only engine that may confirm
3. named-result templates        stdlib      Jensen's *direction*, Markov, AM-GM
4. finite-difference gradients   stdlib      derivative and update-rule claims
5. Z3 / SMT                      optional    decides polynomial arithmetic; can CONFIRM
```

Engine 3 is template matching over the ledger; its output is a side condition and
it joins the same severity path as engine 0. **It is deliberately narrow.** Most
named results need something no parser sees — that a norm is finite, that a
dominating summable bound exists — and those emit nothing rather than a row
saying so. `_shared/latexmath/named.py` lists every catalogued result that is not
checked, with the reason, so "checked and fine" is distinguishable from "not
looked at".

What it does check is worth having: for a convex $f$, $\mathbb{E}[f(X)]$ is the
larger side, and a step that names Jensen, declares its function convex, and puts
that on the smaller side has applied it backwards. That defect sat in the
seeded-error benchmark's *not reachable* list until this engine existed. Where
convexity is **not** declared the direction is unknowable from the source and
nothing is claimed.

Engines 1, 2, 4 and 5 work through **generated check scripts**, one per checkable
step **per engine**, written into `checks/<step>.<engine>.py`. The tool does not translate LaTeX into SymPy: `parse_latex`
needs `antlr4`, and its grammar has no `\mathbb{E}`, no `\operatorname{}`, no
norms and no user macros. A hand-rolled translator's bugs would surface as false
counterexamples, which is the one failure this skill cannot survive.

**So you translate.** Each stub arrives carrying the source LaTeX, the
macro-expanded LaTeX, every symbol's domain *and where that domain came from*, and
the side conditions the step needs. Fill in `build()`, rerun, and the verdict
cites the script — a file the author can open and argue with. See
`checks/_contract.md`, written alongside.

**An unfilled stub reports `untranslatable`**, which composes to `UNVERIFIED`. A
run that translated nothing reports nothing checked, never a clean paper.

## Severity

| Level | Meaning for a proof |
|---|---|
| `CRITICAL` | A reproduced counterexample under a **faithful** translation at a point inside the **stated** domain. Or a structural break: an induction with no base case, a claim dependency cycle. **Says the step as written is false. Does not say the theorem is.** |
| `MAJOR` | Not refuted, but the **licence is missing** — a side condition nowhere assumed, an unjustified limit interchange, a restatement whose hypotheses differ from the body version. *The algebra can be right and the theorem still unproved.* |
| `LOCAL` | Refuted where it stands, and **the refutation was not observed to travel**: the step is a chain row that is not the last, and *every* row after it was independently confirmed. A printed `\lambda T` where the algebra gives `\lambda^T`, on a row whose successor holds either way. *This does not say the result is safe* — only how far the failure was seen to reach. |
| `MINOR` | Impedes checking: an undefined symbol at first use, a `\ref` to nothing, a hedge on a step nothing could verify. |
| `WEAK` | Not refuted by sampling alone, or refuted under a translation that was not faithful. **Not verified.** |
| `UNVERIFIED` | No engine could reach it: opaque operator, unreadable domain, engines disagreed, checker absent, timeout, script rejected. **A finding, not a pass.** |
| `SKIP` | Not an inference, or confirmed symbolically. |

**A dense cluster of `UNVERIFIED` inside one proof is the headline**, not a
footnote. The report's coverage table comes before its findings for that reason.

### `CRITICAL` sometimes means the text is wrong and the result is not

This is the honest reading of the word, and it is written down because a measured
run produced exactly that case and the ladder had no way to say so.

On a validated paper — a monograph whose results are sound and which this skill
had already been driven to zero findings on — a step states a tolerance about five
times looser than the inequality it is used to establish actually supports. Two
independent translations refuted it, faithfully, inside stated domains. It was
hand-checked and the refutation is correct. **The result still stands**, because
downstream that quantity is only ever instantiated well inside the range the
inequality does support.

Every word of the definition above is true of that finding. A reader who sees
`CRITICAL` and concludes *"this theorem is wrong"* has read something the tool did
not say.

So: **a `CRITICAL` is a claim about a step, never about the theorem.** What closes
the gap is the question no engine here answers — *is the refuted step's conclusion
used downstream at a point where it still fails?* Answering it means reading the
paper. `LOCAL` covers the one case that can be settled structurally (the step is a
chain row and every later row was independently confirmed); everything else is
yours.

Two alternatives were built or costed and rejected, and the reasons are worth
keeping. An agent materiality check would catch these, but it builds a mechanism
whose purpose is to argue findings away, and one wrong call there hides a real
defect. A re-check under the restriction the downstream use imposes needs that
restriction to be extractable — measured across ten refutations, **0 of 10** had
one anywhere the ledger models, because the restriction usually lives in prose
outside any proof environment. The case above is in `reference/false-alarms.md`
as entry 23.

Three composition rules, each asserted in `assets/tests/test_compose.py`:

1. An unknown domain can never refute.
2. A translation that is not `faithful` caps severity at `WEAK`.
3. Engines that disagree yield `UNVERIFIED`, never `CRITICAL`.

A fourth demotes rather than suppresses, in `assets/tests/test_supersession.py`:

4. A `CRITICAL` becomes `LOCAL` only when every row after it in the same chain
   was **independently confirmed**. An unchecked later row is not a
   confirmation — silence is not supersession, and that is the property that
   keeps this rung from burying a real defect. A refutation on a chain's last
   row, or outside any chain, is never demoted: it is the conclusion itself
   failing, and nothing can supersede it.

`LOCAL` says the failure did not reach past that row. It does **not** say the
chain's conclusion follows: a broken link is still broken, and confirming the
links after it does not repair the chain.

## Where domains come from

`declared` (the paper says so, with the quote kept) ·
`inferred` (`\sum_{i=1}^n` makes $i$ an integer — honest, usable, never promoted
to declared) · `user-supplied` (`--symbols`) · `unknown` (the default).

Only the first three may license a refutation. When a check fails on a step
carrying an unknown domain, the report says the domain was never stated rather
than naming a counterexample — and lists the symbol so you can supply it.

**Domains are resolved where the step is, not where the symbol first appeared.**
The declarations inside the enclosing proof and its statement are read in source
order, and the last one before the step wins; a symbol the proof says nothing
about keeps whatever the document established. A monograph that declares
$\alpha \in [0,1]$ on page 12 for a convex combination and opens a proof on page
300 with *"for any $\alpha \in (0,1)$"* means the second one there, and reading
the first cost nine `MAJOR` against correct mathematics.

## The structural audit is yours, not the tool's

The tool finds what is mechanical. `reference/structural-audit.md` is the half
that is not, and it is where most real referee findings come from: whether the
hypothesis is *used*, whether quantifier order survives the proof, whether an
inequality points the way the argument needs, whether the induction actually
covers its claim. Work that checklist against every load-bearing proof.

## When a checker is absent

SymPy or Z3 missing is a question for the user, never a `pip install`.
Both are present on the machine this was measured on — sympy 1.12 and
z3-solver 5.1.0. The run
continues: steps routed to that engine become `UNVERIFIED`, the report header
names the checker and its status, and the exit code is `2`.

**Say "nothing wrong was found in a degraded run", not "the proofs are correct".**
They are different sentences and only one of them is true.

## Limits

State these rather than implying completeness.

- **It can refute; it certifies only on a fragment.** An SMT `unsat` is a proof
  that no counterexample exists *under the stated domains*, and Z3 decides
  polynomial real arithmetic — so that fragment is genuinely verifiable. SymPy
  confirms some identities. Everything else is failure to refute, and anything
  with an expectation over an unspecified measure, an integral, a limit or an
  asymptotic is outside the fragment **permanently**, not pending better
  engineering.
- **Measure-theoretic and asymptotic reasoning is out of reach.** `\mathbb{E}` over
  an unspecified measure and $O(\cdot)$ claims are `UNVERIFIED` by construction.
  On three real papers these were the two largest opacity categories.
- **A proof written as running prose rather than `\begin{proof}` is invisible.**
  The report says so instead of reporting a clean document — but measure the cost:
  **2 of 6 papers in the flawed corpus were invisible for exactly this reason**,
  one of them a withdrawn cs.LG paper that declares no theorem environment at all.
  Older and weaker papers are likelier to be written this way, and that is the
  population where errors concentrate.
- **A proof that invokes its own theorem is not reported as circular.** Nothing
  distinguishes "by Theorem 1, which we are proving" from "recall the hypotheses
  of Theorem 1", and the second is what proofs actually do. Genuine multi-claim
  cycles are still caught.
- **The sandbox is not a security boundary.** It is a guard against a generated
  script importing `os`, touching the paper directory, or looping forever.
- **No local ground truth exists for proofs.** The benchmark uses seeded errors,
  which are cleaner than real ones and overstate recall. The honest headline is
  the false-alarm rate on untouched correct derivations.

## Measured results

**Seeded-error benchmark** (`assets/tests/test_seeded_errors.py`, offline and
deterministic — run it yourself). Six realistic defects injected into correct
derivations, each paired with its untouched original:

| | |
|---|---|
| Seeded defects detected | **6 of 6** |
| **False alarms on the correct originals** | **0 of 6** |
| `CRITICAL` or `MAJOR` raised against correct mathematics | **0** |

Five further defect classes — a flipped inequality, a sign error, an off-by-one
summation bound, Jensen applied the wrong way, a swapped quantifier — are **not
reachable by the default engines** and are listed as such in the benchmark rather
than quietly omitted. The first three need a translated check script; the last
needs a reader working `reference/structural-audit.md`.

**Real papers, against known ground truth.** Thirteen arXiv papers: **six with a
documented, localised defect** (three author withdrawals naming the lemma, two
published corrections naming the bound) and **seven validated** — two of them
reference monographs, two the corrections themselves. Proof text segmented
**100%** on every one.

| | papers | CRITICAL | MAJOR | papers with any |
|---|---|---|---|---|
| **validated** | 7 | 0 | 5 | 2 of 7 |
| **documented defect** | 6 | 0 | **0** | **0 of 6** |

Re-measured 2026-08-15 by an acceptance benchmark that fetches all thirteen
e-prints and runs the shipped entry point. Every number in this section comes
from that run.

**Seven further papers, none in that corpus**, were run to find out whether the
false-alarm rate had settled. It has not, and the shape of the answer is more
useful than the answer:

| Fresh paper | steps | new false-alarm classes |
|---|---|---|
| quantum Shannon theory | 2692 | **0** |
| online-learning monograph | 1494 | **5** |
| matrix-concentration monograph | 540 | **3** |
| bandit survey | 470 | 0 |
| computational optimal transport | 178 | 0 |
| Rényi differential privacy | 122 | 0 |
| PAC-Bayes primer | 59 | 0 |
| wide-network analysis | 37 | 0 |

The two monographs that came before the fixes produced new classes; nothing under
500 steps ever has.
Eight of those classes (14–21 in `reference/false-alarms.md`) were found and
fixed. Six of the eight are *wrong domains* — a symbol given a range it does not
have, recorded as `declared`, which is a refuting provenance. That is the worst
failure available to this skill: the tool becomes entitled to evaluate a step
outside the paper's meaning and report a counterexample against correct
mathematics.

The reason long documents dominate is not subtle. They reuse their letters. `t`
is a round index in one chapter and a convex weight in another, `a` is bounded on
one page and free on the next, and every rule that reads a domain from *somewhere
in the document* rather than *here* breaks on exactly that.

**The stopping criterion, and where it stands.** "Further papers with no new
class" proved unreachable, so it is a rate: **a fresh document of at least 500
steps yielding fewer than one new false-alarm class per 1000 steps.** The
monographs measured 3.3 and 5.6 before their classes were fixed. The 2692-step
quantum-information book, run afterwards and four times the size of anything else
tested, measured **0.0 — the criterion is met.** Its four `MAJOR` are one
recurrence of an existing class and three legitimate findings, each a proof
dividing by or taking the logarithm of a quantity whose stated range includes
zero.

**One document is one document.** And the same run turned up a defect of a
different kind that no amount of false-alarm counting would have caught: **158
step ids collided** on it, because a claim proved twice produced two proofs with
the same id. Re-checking found 24 more on one corpus paper and 16 on another that
had been there from the beginning. Nothing failed — a duplicate id silently
wins — and a verdict computed on one proof had been reported against a step in
another. See class 22.

Two of the eight classes were caught by nothing but the acceptance benchmark:
a fix that passed the entire unit suite put a `MAJOR` back on Bubeck — the
corpus's most heavily vetted document — and a second one silently removed four
genuine findings. Both surfaced only on re-running the thirteen papers.

**The finite-difference engine, on a derivative a real paper states.** Wilde's
calculus lemma behind Pinsker's inequality defines
$g(a,b)= a\ln(a/b)+(1-a)\ln\frac{1-a}{1-b}-2(a-b)^2$ and states
$\partial g/\partial b$. That derivative is correct and the engine returns
`not-refuted`; perturbing the stated coefficient from 4 to 2 is refuted at
$a=0.3,\ b=0.5$ with both values printed. Both directions ship as
`assets/tests/test_gradient_on_a_real_claim.py` — an engine whose only
demonstration is finding an error says nothing about how often it invents one.

**With a translated check script it is a different tool.** Given the step ledger
and one filled-in `build()`, the SymPy engine **exactly refuted** Adam's
Lemma 10.4 step 10 — the step arXiv:1804.10587 exists to correct:

```
rhs - lhs = -29*sqrt(3)/48 + sqrt(2)/16 + 3/16   (~ -0.771)
```

at $T=4,\ \gamma=1/2,\ \beta_2=0$, all gradient norms 1 — every value inside the
domains the paper states. The violation is robust: false at 13 of 20 parameter
settings tried, growing with $T$ as the asymptotics demand.

**And `--symbols` is not optional — nor, now, is it unaided.** On the 2692-step
quantum-information book, 63 of 88 symbols had no readable domain.
`--emit-symbols-template` ranks them by how many unmet obligations each one
stands in rather than by how often it appears, because a symbol used 900 times in
settled steps is worth less than one used twice in a denominator. Filling in the
**top seven of 63** discharged **44 of 572** unmet side conditions and produced no
new finding of any severity.

**And `--symbols` is not optional.** That refutation was initially **suppressed**,
because Adam never states domains for $T$, $\gamma$ or $\beta_2$ and an unknown
domain may not refute. The guard that prevents false alarms had hidden a true one.
It now reports `refutation-blocked-by-unknown-domain` at `MAJOR`, naming the
symbols to supply — and with them supplied the same step returns `CRITICAL`.
**A blocked decisive check is the most actionable thing this skill produces.**

**False alarms.** Every rule in `reference/false-alarms.md` was earned on a real
paper. Twenty-two entries so far, including: 4 fabricated `CRITICAL`s from an
induction detector that hard-coded the variable name; 54 spurious opacity reasons
from `\operatorname{\mathbb{E}}`; `\sqrt{t}` under `\sum_{t=1}^{T}`, which fired
on every optimization paper; `\rho^{-1}` on a scalar step size reported as
needing matrix invertibility; sibling theorems in a family read as restatements;
`differentiate-under-integral` fired on Taylor's theorem with integral remainder;
`y_t \in [0,1]` read as a declaration about the subscript $t$; one `x \ge 0`
declaring seven symbols at once; `\varepsilon \leq 0.006` read as
`\varepsilon \leq 0`; and `\int_0^\infty f = \lim_L \int_0^L f` reported as an
unjustified interchange when it is the definition.

**Net effect on the validated set: 14 `MAJOR` → 5, and 0 fabricated `CRITICAL`s
throughout.** Bubeck's monograph — at 451 steps the largest and most heavily
vetted document in either corpus — went from 7 `MAJOR` to **zero**.

## See also

- `reference/structural-audit.md` — the non-mechanical checklist, and what each
  failure looks like in the source
- `reference/engines.md` — what each engine can and cannot license
- `reference/step-ledger.md` — the schema, field by field
- `reference/false-alarms.md` — every false alarm observed, and the rule that
  killed it
- `explaining-derivations` — consumes these verdicts to expand a proof step by
  step, and treats a step it cannot expand as evidence against the derivation
- `reviewing-paper-sources` — phase 0 offers this skill; phase 4 invokes it
- Shared parsing layer: `_shared/latexmath`