Rigorous mathematical proof verification and fixing workflow. Reads a LaTeX proof, identifies gaps via cross-model review (external reviewer backend, ultra reasoning), fixes each gap with full derivations, re-reviews, and generates an audit report. Use when user says "检查证明", "verify proof", "proof c

Proof Checker: Rigorous Mathematical Verification & Fixing 🔒 Do not wrap this skill in /loop , /schedule , or CronCreate . It is verdict bearing — it judges proof validity across rounds, threading the reviewer's memory from Phase 1 → Phase 3 via codex reply so the reviewer can check whether a fix actually closed the gap it flagged. An external timer re enters from the top each tick, starting a fresh thread and losing that memory. Schedule the external wait that precedes it , not the verdict. See [ shared references/external cadence.md ](../shared references/external cadence.md). Systematically verify a mathematical proof via cross model adversarial review, fix identified gaps, re review until convergence, and generate a detailed audit report with proof obligation accounting. Context: $ARGUMENTS Constants MAX REVIEW ROUNDS = 3 REVIEWER MODEL = gpt 6 astra — Default model for the Codex backend, reasoning effort ultra (deep audit tier; capability fallback gpt 6 astra + xhigh → gpt 5.5 + xhigh per shared references/reviewer routing.md , capability errors only — never below xhigh ). Manual backend uses a model the user chooses, but it must be a non Claude model ARIS can classify (OpenAI, Google, DeepSeek, Moonshot/Kimi, Qwen) — the executor is Claude, so routing the proof review into any Claude product makes Claude judge Claude and voids the cross model invariant (see shared references/reviewer routing.md ). REVIEWER BACKEND = codex — Default: Codex MCP (ultra). Override with — reviewer: oracle pro for Oracle MCP, or — reviewer: manual for Manual Review MCP. If manual review MCP is unavailable, stop and print the install command; do not fall back to Codex. See shared references/reviewer routing.md . Reviewer Calling Convention When calling the reviewer, branch on REVIEWER BACKEND: If REVIEWER BACKEND = codex : Use mcp codex codex for new review threads ( model: gpt 6 astra , config: {"model reasoning effort": "ultra"} ). Use mcp codex codex reply for follow up rounds (reuse threadId). If REVIEWER BACKEND = manual : Use mcp manual review review for new review threads with: prompt: [exact same prompt that would go to Codex] config: {"model reasoning effort": "xhigh", "executor model": "<actual executor model ", "require reviewer model": true} Save the returned threadId . Use mcp manual review review reply for follow up rounds with: threadId: [saved manual review threadId] prompt: [follow up prompt] config: {"model reasoning effort": "xhigh", "executor model": "<actual executor model ", "require reviewer model": true} Prompt fidelity: the manual prompt must be exactly the same text that Codex would receive. Review tracing applies equally to both backends. AUDIT DOC: PROOF AUDIT.md at the paper directory root, alongside main.tex (cumulative log; when invoked via /paper writing , this is paper/PROOF AUDIT.md ) REPORT TEX: proof audit report.tex (formal before/after PDF) STATE FILE: PROOF CHECK STATE.json (for recovery) SKELETON DOC: PROOF SKELETON.md (micro claim inventory) RENDER HTML = true — When true (default), auto render PROOF AUDIT.md to HTML at workflow end via /render html . Uses full Codex review gate (audit class artifact — math heavy content; render fidelity check protects against MathJax breakage and matches the skill's cross model audit invariant). Set false to skip, or pass — render html: false . Acceptance Gate (objective, replaces subjective scoring) The proof passes when ALL of the following hold: 1. Zero open FATAL or CRITICAL issues 2. Every theorem/lemma has: (i) explicit hypotheses, (ii) proof with all interchanges justified, (iii) every application discharges hypotheses in the ledger 3. All big O/Θ/o statements have declared parameter dependence and uniformity scope 4. Counterexample pass executed on all key lemmas (log candidates even if none found) Issue Taxonomy (20 categories, 4 groups) Group A: Logic & Proof Structure Category Description Example UNJUSTIFIED ASSERTION Claim stated without proof or reference "The Hessian splits into Gram blocks" UNPROVEN SUBCLAIM "Clearly" / "it follows" hides a nontrivial lemma "By symmetry, the cross terms vanish" without checking QUANTIFIER ERROR Wrong order ∀/∃, missing "for sufficiently small κ" "For all π, there exists ε" vs "there exists ε for all π" IMPLICATION REVERSAL Uses (A⇒B) as (B⇒A), or claims equivalence with only one direction CASE INCOMPLETE Misses boundary/degenerate cases Singular covariance, zero weight, non unique argmin CIRCULAR DEPENDENCY Lemma uses theorem that depends on it LOGICAL GAP A step is not justified by what precedes it B=Θ(1) → β K=0 without analyzing W Group B: Analysis & Measure Theory Category Description Example ILLEGAL INTERCHANGE Swaps limit/expectation/derivative/integral without DCT/MCT/Fubini Differentiating under E without domination NONUNIFORM CONVERGENCE Pointwise convergence used as uniform sup and limit swapped MISSING DOMINATION DCT cited but no dominating function given INTEGRABILITY GAP Uses E X ^p without proving/assuming finite moments REGULARITY GAP Differentiability/Lipschitz/convexity used but not established STOCHASTIC MODE CONFUSION Mixes a.s./in prob./in L²/in expectation Group C: Model & Parameter Tracking Category Description Example MISSING DERIVATION A quantity is used but never derived from the model Risk functional with undefined B, W HIDDEN ASSUMPTION Proof silently uses a condition not in the theorem Gaussianity assumed but not stated INSUFFICIENT ASSUMPTION Hypotheses too weak for proof (counterexample exists) Moment conditions admitting 2 point distributions DIMENSION TRACKING Parameter dependence (d, n, K, ...) not explicit d enters only through κ NORMALIZATION MISMATCH Coordinate/scaling conventions inconsistent Rescaled vs raw coordinates CONSTANT DEPENDENCE HIDDEN "C" depends on d,n,K but treated as universal Group D: Scope & Claims Category Description Example SCOPE OVERCLAIM Conclusion stated more broadly than proof supports "β K=0" with only generic overlap REFERENCE MISMATCH Cited theorem's hypotheses not verified at point of use Two Axis Severity System Axis A — Proof Status (what is wrong) Status Meaning INVALID Statement false as written (counterexample exists or contradiction) UNJUSTIFIED Could be true, but current proof does not establish it UNDERSTATED True only after strengthening assumptions OVERSTATED True only after weakening conclusion / adding qualifiers UNCLEAR Ambiguous notation / definition drift (not wrong per se) Axis B — Impact (how much breaks) Impact Meaning GLOBAL Breaks main theorem or core dependency chain LOCAL Affects a side result but not the main theorem COSMETIC Exposition only Severity Labels (derived) Label Definition FATAL INVALID + GLOBAL CRITICAL (INVALID + LOCAL) or (UNJUSTIFIED + GLOBAL) MAJOR (UNJUSTIFIED + LOCAL) or (UNDERSTATED/OVERSTATED + GLOBAL) MINOR Clarity / notation / dimension bookkeeping that doesn't change claims Side Condition Checklists for Common Theorems When the proof invokes any of the following, require explicit verification of ALL listed conditions: Theorem Required Conditions DCT (Dominated Convergence) Pointwise a.e. convergence + integrable dominating function MCT (Monotone Convergence) Monotone increasing + non negative Fubini/Tonelli Product measurability + integrability (Fubini) or non negative (Tonelli) Leibniz integral rule Continuity of integrand + dominating function for derivative Implicit Function Theorem Continuous differentiability + non singular Jacobian Taylor with remainder Sufficient differentiability + remainder form (Lagrange/integral) Jensen's inequality Convexity of function + integrability Cauchy Schwarz Correct inner product space + integrability of both factors Weyl/Davis Kahan Symmetry/Hermiticity + perturbation bound conditions Analytic continuation Domain connectivity + identity theorem conditions WLOG reduction Invariance under claimed symmetry + reduction is reversible Workflow Phase 0: Preparation 1. Locate the proof : Find the main .tex file(s). 2. Read the entire proof : Extract list of all theorems/lemmas/propositions/corollaries/definitions/assumptions. 3. Read reference materials : Reference papers, prior results. 4. Build a section map : Structured list with line numbers and key claims. 5. Identify the main theorem : Central result, assumptions, claims. Phase 0.5: Proof Obligation Ledger Fan out (Tier aware) — build the ledger in parallel; never judge in parallel. For a large multi theorem paper, ledger construction is breadth over independent sections. Tier 1 (Workflow): spawn one Claude subagent per section/theorem to extract that unit's symbols, assumptions, micro claims, and local quantified statements, each returning a structured ledger fragment. Tier 2 : the same subagents via the Agent tool. Tier 3 : walk the sections sequentially. This follows [ shared references/fan out pattern.md ](../shared references/fan out pattern.md). Two hard rules: 1. The shards EXTRACT, they do not ADJUDICATE. Building the ledger (inventorying obligations, typing symbols, restating with explicit quantifiers) is structural extraction. Whether a proof step is valid — whether an obligation is actually discharged — is a Type B correctness verdict reserved for the cross model jury in Phase 1 / Phase 3 (codex or manual, ultra ). A Claude shard MUST NOT mark a micro claim "proved" or "sound"; it only records the obligation and where the paper claims to discharge it. See [ acceptance gate.md ](../shared references/acceptance gate.md) — the loop may self verify that the ledger is complete , never that the proofs are correct . This governs the ledger spec wording below. Where the artifacts say "WHERE each is verified", "or mark UNVERIFIED", or "where conditions are proven", a shard records a location pointer ( file:line the paper claims discharge) — never its own judgment that the discharge is mathematically valid. A shard's UNVERIFIED means "the paper cites no discharge location" , NOT "the shard checked the math and it fails" . Soundness is the jury's verdict, not the shard's. Shard output (extraction schema, per [ fan out pattern.md ](../shared references/fan out pattern.md)): each shard returns {shard id: "<section/theorem id ", entries: [...]} — the typed ledger items (symbols, assumptions, micro claims, canonical statements, limit order facts) for that unit, each carrying its canonical id (e.g. MC 17 , the symbol name) as dedup key . Never prose only; never a validity verdict field. 2. Global artifacts are a barrier, computed on the merged ledger, not per shard. The Dependency DAG and its cycle detection (incl. semantic circularity), and cross section symbol type consistency, require the whole paper in view. Merge all shard fragments first, then compute these on the union — a per shard DAG would miss exactly the cross section cycles this phase exists to catch. Build formal accounting artifacts. Save to PROOF SKELETON.md : 1. Dependency DAG Nodes = Definitions / Assumptions / Lemmas / Theorems. Edges = "uses". Detect cycles (including semantic circularity where Lemma A uses a corollary that quietly depends on A)

proof-checker