# 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. - **Type:** Skill - **Install:** `agentstack add skill-chgagne-claude-skills-research-verifying-proofs` - **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior - **Seller:** [chgagne](https://agentstack.voostack.com/s/chgagne) - **Installs:** 0 - **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills) - **Latest version:** 0.1.0 - **License:** MIT - **Upstream author:** [chgagne](https://github.com/chgagne) - **Source:** https://github.com/chgagne/claude-skills-research/tree/main/verifying-proofs ## Install ```sh agentstack add skill-chgagne-claude-skills-research-verifying-proofs ``` Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent. ## About # 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/..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 ..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 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](https://github.com/chgagne) - **Source:** [chgagne/claude-skills-research](https://github.com/chgagne/claude-skills-research) - **License:** MIT Install and usage instructions live in the source repository linked above. ## Pricing - **Free** — Free ## Security capabilities Automated source analysis of v0.1.0 — what this tool can access: - **Network access:** no - **Filesystem access:** no - **Shell / process execution:** no - **Environment & secrets:** no - **Dynamic code execution:** no *"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.* ## Versions - **0.1.0** — security scan: passed — Imported from the upstream source. ## Links - Listing page: https://agentstack.voostack.com/l/skill-chgagne-claude-skills-research-verifying-proofs - Seller: https://agentstack.voostack.com/s/chgagne - Browse the marketplace: https://agentstack.voostack.com/browse --- Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.