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

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

# 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 ..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:

1. 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 ever

…

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: chgagne
• Source: chgagne/claude-skills-research
• License: MIT

Install and usage instructions live in the source repository linked above.