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