skills/proof-audit/SKILL.md

---
name: proof-audit
description: >-
  Adversarially audit an existing mathematical claim, proof, derivation, diagram, or theorem dependency for correctness. Use for requests to verify, referee, stress-test, type-check, find gaps, or isolate the exact remaining implication. Default to read-only. Do not use to invent a substantially new proof route or merely copyedit prose.
---

# Mathematical proof audit

Audit the claim actually stated, under its stated hypotheses. Do not rescue it
by changing definitions, conventions, or scope.

## Establish the target

1. Determine the repository root and read applicable instructions.
2. Resolve current proof, status, claims, conventions, literature, and
   verification roles from project instructions or standard filenames.
3. Restate the claim as a claim card:
   - quantified objects and exact conclusion;
   - hypotheses and exceptional cases;
   - source and target, coefficient domain, grading, variance, signs,
     finiteness/completion, equivariance, and range;
   - evidence label, dependencies, and cited computation or source.
4. If the statement cannot be typed unambiguously, report that before auditing
   the argument.
5. Resolve the authoritative statement itself, not only a dashboard summary.
   Record its exact locator or revision when nearby material can change without
   changing the claim.

## Build the dependency graph

When the project has a `.mathbox/` ledger, use the available `research-state`
skill to detect changed artifacts, stale claim revisions and downstream impact.
Inspect the raw current proof even when the ledger reports `proved`. Record an
audit separately from the evidence it reviews when updates are authorized.
If those updates are authorized but this host cannot execute or write, use the
`research-state` deferred-handoff contract for the audit report and review
proposal; state that it has not been recorded.

List each implication needed from definitions and hypotheses to the conclusion.
Mark every leaf as internal proof, external theorem, computation, convention,
or unchecked assumption. Detect circular dependencies and claims whose evidence
ultimately points back to the claim itself.

## Audit adversarially

For every applicable obligation:

- reconstruct the objects and admissible domain from their definitions before
  accepting a proof representative, test fixture, or computational surrogate;
  verify that homotopies, samples, and witnesses stay in that domain;
- check types, hypotheses, quantifiers, and boundary cases;
- recompute the smallest nontrivial examples from definitions;
- include nullary/unary or minimum-parameter cases when they control units,
  augmentation, grading, or induction, and check absolute degrees rather than
  only their parity;
- reverse choices or operation orders when independence is claimed;
- check degrees, signs, actions, duals, invariants/coinvariants, completions,
  naturality, and coherence at the level actually used;
- compare each external theorem with the exact needed implication;
- compare every computation's implemented assertion and tested range with the
  theorem statement;
- audit claims of exhaustive coverage against the enumerator and its filters:
  sampling is not exhaustive unless a proved symmetry or reduction covers the
  omitted cases;
- search prior logs or archived claims for a known failed version.

When an external-source leaf is not already verified in the project's durable
literature record, route the source question through the available
`literature-check` skill (`mathbox:literature-check` in plugin installations).
That workflow checks an authorized project-local cache before fetching. If the
skill is unavailable, perform the exact-source check with available tools. When
the exact source cannot be checked, mark the leaf **conditional**; do not fill
it from a snippet, secondary citation, or memory.

Load the relevant domain sections of
[obligation-checklists.md](references/obligation-checklists.md); do not apply
irrelevant checklists mechanically.

Mark each obligation **passed**, **failed**, **conditional**, **not addressed**,
or **out of scope**. Agreement on notation or small cases is not proof of a
universal statement.

## Verdict

Return exactly one primary verdict:

- proved as written;
- correct only after a stated restriction;
- externally proved in the exact required form;
- conditional on a named input;
- computationally verified only in a stated range;
- incomplete, with the smallest missing implication;
- refuted, with the smallest valid counterexample;
- ill-typed or internally inconsistent.

Default to no edits. When the user also requests correction, change the durable
proof and dependent status only after identifying the failed implication and
reviewing the blast radius. A convention change still requires the project's
normal approval.

## Output

Lead with the normalized claim and verdict. Then give:

1. dependency graph;
2. obligation matrix;
3. decisive evidence or counterexample;
4. source/computation checks and commands;
5. exact remaining gap;
6. strongest safe statement and cheapest next check.

For an independent audit, use a fresh session or isolated subagent when the
tool supports it and delegation is authorized. Give the exact claim and raw
proof/source artifacts, without the author's verdict or suspected gap. Ask for
a fresh derivation of the critical implication and of the object being tested.
Do not give it an implementation or geometric surrogate as though that were the
definition. Otherwise label the pass self-review. Neither agreement between
agents nor a different actor name proves independence or mathematical
correctness; successive reviews can share the same model error.