Adversarial audit of mathematical proofs, derivations, and formal environments
Structured adversarial audit of mathematical content: proofs, derivations, definitions, assumptions, and formal environments. Works on any section containing formal math.
/audit-math appendix-a -- full audit of Appendix A/audit-math methodology -- audit math content in the methodology section/audit-math 200-450 -- audit specific line range in main.texThe user provides one of:
appendix-a, methodology, results)200-450).claude/rules/notation-protocol.md for custom commands, core variables, subscript conventions, theorem environment numbering, and math writing rules (if it exists)guidance/paper-context.md for key labels, formal environment ordering, and canonical results (if it exists).claude/rules/academic-writing.md for cross-reference style rules and terminologymain.tex using %% BEGIN/END markers (or line range)Build a registry of every formal environment in the target section:
\begin{definition})\begin{assumption})\begin{lemma})\begin{proposition})\begin{corollary})\begin{theorem})\begin{proof})\begin{remark})For each, record: label, name (from [...] bracket), line number, and which assumptions/results it references.
If notation-protocol.md registers environment numbering, cross-check against it. Flag any missing or extra environments, misordered labels, or mismatched names.
For each lemma, proposition, corollary, and theorem:
\ref{assum:...} (not prose descriptions like "the independence assumption")Present as a table:
| Result | States | Uses | Hidden | Unused |
|---|
For each proof, check:
\begin{proof} have a matching \end{proof}?For each inequality or signed result:
Test each result at the edges of its parameter space:
Using notation-protocol.md as the reference (if available):
\E[...] not E[...], \Var not \text{Var}, etc.)\ref{...} to a definition, assumption, lemma, proposition, corollary, or theorem must point to a valid \label{...}\eqref{...} (not \ref{...})Eq.~\eqref{...}, Lemma~\ref{...}, Assumption~\ref{...}Each formal result should be followed by interpretive prose. Check:
If the target section contains no formal environments:
/audit-section [key] for a general content audit instead."MATH AUDIT: [section name / line range]
========================================
ENVIRONMENT INVENTORY:
Definitions: N (labels: ...)
Assumptions: N (labels: ...)
Lemmas: N
Propositions: N
Corollaries: N
Theorems: N
Proofs: N
Remarks: N
Inventory vs notation-protocol.md: [MATCH / N discrepancies / not available]
ASSUMPTION DEPENDENCIES:
| Result | States | Uses | Hidden | Unused |
|--------|--------|------|--------|--------|
| Lemma 1 | none | none | -- | -- |
| Prop 1 | 1,2 | 1,2 | -- | -- |
| ... | ... | ... | ... | ... |
PROOF COMPLETENESS: [N issues]
- [Line X] [SEVERITY]: [description]
SIGN ANALYSIS: [N issues]
- [Line X] [SEVERITY]: [description]
BOUNDARY CASES: [N issues]
- [Line X] [SEVERITY]: [description]
NOTATION CONSISTENCY: [N issues]
- [Line X] [SEVERITY]: [description]
CROSS-REFERENCES: [N issues]
- [Line X] [SEVERITY]: [description]
INTERPRETIVE PROSE: [N issues]
- [Line X] [SEVERITY]: [description]
SEVERITY SUMMARY:
CRITICAL: N (errors that invalidate a result or hide a dependency)
IMPORTANT: N (gaps that a referee would flag)
MINOR: N (notation inconsistencies, style issues)
NICE-TO-HAVE: N (polish items)
TOP PRIORITY FIXES:
1. [CRITICAL] [Line X]: [description and suggested fix]
2. [IMPORTANT] [Line Y]: [description and suggested fix]
3. [etc.]
This skill can be called from /full-paper-audit as an additional pass on sections containing formal math. The recommended integration point is after Step 2 (section-by-section audit):
Step 2b: For sections containing formal environments (any appendix or main body
section with \begin{proposition}), run /audit-math.
When called from /full-paper-audit, suppress the full output template and return only the SEVERITY SUMMARY and TOP PRIORITY FIXES sections.