What problem does it solve? Mathematical proofs in research papers often contain hidden gaps, unjustified steps, illegal limit interchanges, and unstated assumptions that are hard to catch by self-review. This Skill rigorously verifies LaTeX proofs using an external non-Claude reviewer model, fixes each identified gap with full derivations, and produces a formal audit report. ## Core Features & Use Cases - Cross-Model Adversarial Review: Submits proofs to an external reviewer backend (Codex or Manual Review MCP) at xhigh reasoning effort across up to 3 review rounds, threading reviewer memory so fixes are checked against the original gaps. - Structured Issue Taxonomy: Classifies findings across 20 categories in 4 groups (logic, analysis/measure theory, parameter tracking, scope) with a two-axis severity system (FATAL/CRITICAL/MAJOR/MINOR). - Proof-Obligation Ledger: Builds a dependency DAG, assumption ledger, typed symbol table, canonical quantified statements, and micro-claim inventory before review. - Fix & Re-Review Loop: Implements fixes directly in the .tex file (with optional --deep-fix repair-grade plans), runs counterexample red-teaming, blind re-review of FATAL/CRITICAL fixes, and optional --restatement-check for theorem statement drift. - Use Case: A researcher finishing a theory paper runs the checker on main.tex; it flags an unjustified dominated-convergence interchange in Lemma 3, derives the missing domination argument, patches the LaTeX, and emits PROOF_AUDIT.md plus a formal proof_audit_report.tex. ## Quick Start Ask the assistant to run the proof-checker skill on your paper's main.tex file to verify every theorem and lemma and generate an audit report.
