verifying-proofslisted

# 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