Update to Mathbox

{
  "description": "Adversarially audit an existing mathematical claim, proof, derivation, diagram, or theorem dependency for correctness. Use to verify, check, stress-test, type-check or find gaps in a single claim, proof or dependency. Do not use for a whole-manuscript referee report, inventing a substantially new proof route, or merely copyediting prose.",
  "included_files": [
    {
      "relative_path": "agents/openai.yaml",
      "size_in_bytes": 254
    },
    {
      "relative_path": "evals/evals.json",
      "size_in_bytes": 6175
    },
    {
      "relative_path": "evals/trigger-evals.json",
      "size_in_bytes": 1433
    },
    {
      "relative_path": "references/obligation-checklists.md",
      "size_in_bytes": 2886
    }
  ],
  "name": "proof-audit",
  "skill_md_contents": "---\nname: proof-audit\ndescription: >-\n  Adversarially audit an existing mathematical claim, proof, derivation, diagram, or theorem dependency for correctness. Use to verify, check, stress-test, type-check or find gaps in a single claim, proof or dependency. Do not use for a whole-manuscript referee report, inventing a substantially new proof route, or merely copyediting prose.\n---\n\n# Mathematical proof audit\n\nAudit the claim actually stated, under its stated hypotheses. Do not rescue it\nby changing definitions, conventions, or scope.\n\nFor a referee-style assessment of an entire manuscript, use the available\n`referee` skill (`mathbox:referee` in plugin installations). This skill remains\nresponsible for focused mathematical obligations delegated by that review.\n\n## Establish the target\n\n1. When auditing project files, read applicable instructions and resolve the\n   authoritative statement, proof, status, conventions, literature record and\n   verification commands, recording its locator or revision rather than a summary.\n2. Restate the claim as a claim card:\n   - quantified objects and exact conclusion;\n   - hypotheses and exceptional cases;\n   - source and target, coefficient domain, grading, variance, signs,\n     finiteness/completion, equivariance, and range;\n   - the project's recorded evidence label, dependencies, and cited computation or source.\n3. If the statement cannot be typed unambiguously, return the ill-typed verdict;\n   continue only under explicitly labelled readings.\n\n## Build the dependency graph\n\nWhen the project has a `.mathbox/` ledger, use the available `research-state`\nskill to detect changed artifacts, stale claim revisions and downstream impact.\nInspect the raw current proof even when the ledger reports `proved`. Record an\naudit separately from the evidence it reviews when updates are authorized.\nIf those updates are authorized but this host cannot execute or write, use the\n`research-state` deferred packet contract for the audit report and review\nproposal; state that it has not been recorded.\n\nList each implication needed from definitions and hypotheses to the conclusion.\nMark every leaf as internal proof, external theorem, computation, convention,\nor unchecked assumption. Detect circular dependencies and claims whose evidence\nultimately points back to the claim itself.\n\n## Audit adversarially\n\nFor every applicable obligation:\n\n- reconstruct the objects and admissible domain from their definitions before\n  accepting a proof representative, test fixture, or computational surrogate;\n  verify that homotopies, samples, and witnesses stay in that domain;\n- check types, hypotheses, quantifiers, and boundary cases;\n- recompute the smallest nontrivial examples from definitions;\n- include nullary/unary or minimum-parameter cases when they control units,\n  augmentation, grading, or induction, and check absolute degrees rather than\n  only their parity;\n- reverse choices or operation orders when independence is claimed;\n- check degrees, signs, actions, duals, invariants/coinvariants, completions,\n  naturality, and coherence at the level actually used;\n- compare each external theorem with the exact needed implication;\n- compare every computation's implemented assertion and tested range with the\n  theorem statement;\n- audit claims of exhaustive coverage against the enumerator and its filters:\n  sampling is not exhaustive unless a proved symmetry or reduction covers the\n  omitted cases;\n- search prior logs or archived claims for a known failed version.\n\nRoute unchecked external leaves through the available `literature-check` skill\n(`mathbox:literature-check` in plugin installations), or check exact sources\ndirectly if unavailable; mark the obligation conditional if unverifiable.\nRoute load-bearing computations through the available `computation-audit` skill\n(`mathbox:computation-audit` in plugin installations), or apply the finite-assertion,\nrange and coverage checks above directly.\n\nLoad the relevant domain sections of\n[obligation-checklists.md](references/obligation-checklists.md); do not apply\nirrelevant checklists mechanically.\n\nMark each obligation **passed**, **failed**, **conditional**, **not addressed**,\nor **out of scope**. Agreement on notation or small cases is not proof of a\nuniversal statement.\n\n## Verdict\n\nReturn exactly one primary verdict:\n\n- proved as written;\n- correct only after a stated restriction;\n- externally proved in the exact required form;\n- conditional on a named input;\n- computationally verified only in a stated range;\n- incomplete, with the smallest missing implication;\n- refuted, with the smallest valid counterexample;\n- ill-typed or internally inconsistent.\n\nDefault to no edits. Never close a gap with a new argument. Requested corrections\nmay only restrict the statement or fix a forced local step, after reviewing\ndownstream dependents. Label other repairs unaudited, retain the verdict and\nroute new arguments through the available `research-attempt` skill\n(`mathbox:research-attempt` in plugin installations), or return the exact research\nobligation if unavailable. Propagate into a manuscript only on explicit request\nthrough the available `manuscript-integrate` skill (`mathbox:manuscript-integrate`\nin plugin installations), or preserve its validation/edit boundaries directly.\nConvention changes require the project's normal approval.\n\nFor ledger reviews, use `pass` only when the verdict supports the evidence's\nexact claim, `conditional` for a conditional verdict, and `fail` otherwise.\nA restriction or finite range does not pass evidence asserting the full claim.\n\n## Output\n\nLead with the normalized claim and verdict. Then give:\n\n1. dependency graph;\n2. obligation matrix;\n3. decisive evidence or counterexample;\n4. source/computation checks and commands;\n5. exact remaining gap;\n6. strongest safe statement and cheapest next check;\n7. review provenance (self-review or independent) and exact revision audited.\n\n## Independence\n\nWhen the user or project requires an independent audit, use a fresh session or\nisolated subagent when the\ntool supports it and delegation is authorized. Give the exact claim and raw\nproof/source artifacts, without the author's verdict or suspected gap. Ask for\na fresh derivation of the critical implication and of the object being tested.\nDo not give it an implementation or geometric surrogate as though that were the\ndefinition. Otherwise label the pass self-review. Neither agreement between\nagents nor a different actor name proves independence or mathematical\ncorrectness; successive reviews can share the same model error.\n"
}