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 Before each reviewer slot , follow [Selectable Reviewers](../shared references/reviewer backends.md): resolve invocation → .aris/reviewer.json → Claude Code default (Codex MCP) with reviewer route.py through the canonical helper resolver, preserving this slot's tier, fresh contexts, source/image inputs and deterministic gates. Codex examples/pins below apply only to backend=codex ; other routes use their own first call/reply contract. Save the route and actual returned identity; unavailable selections are REVIEW UNAVAILABLE . Classify acceptance from actual families/completion/scope. Forward invocation reviewer/model/effort overrides to reviewer bearing children. Generation workers are unchanged. 🔒 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; per shared references/reviewer routing.md , capability fallback gpt 6 astra + xhigh then the model capability fallbacks starting with gpt 6.1 sol + xhigh , 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 Bounded fan out — build the ledger in parallel; never judge in parallel. Freeze mechanically enumerable source unit IDs before dispatch: file spans, sections, theorem/lemma/proposition blocks, or proof environments with stable source anchors. Sort them by source order and partition them into no more than max shards: 8 . Run waves of at most max concurrency: 4 , with max turns: 8 per leaf. Obligations are discovered from these units and receive deterministic IDs only after extraction , derived from the source unit ID plus a stable ordinal or anchor (for example THM 3:OB 004 ). Tier 1 (Workflow): explicitly select aris fanout leaf for every shard. Tier 2 (Agent): call only Agent(aris fanout leaf) . Tier 3 : process the same frozen shards sequentially. A failed, malformed, or timed out shard gets at most one executor side sequential fallback and never a replacement Agent. This follows [ shared references/fan out pattern.md ](../shared references/fan out pattern.md). The leaf prompt repeats the assigned IDs, no delegation, read only, no verdict, and output schema rules because workers do not inherit this skill. 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 is a Type B correctness verdict reserved for the cross model jury in Phase 1 / Phase 3. A leaf MUST NOT mark a micro claim "proved" or "sound"; it only records the obligation and the location where the paper claims to discharge it. A shard's UNVERIFIED means the paper cites no discharge location, not that the leaf checked the mathematics and rejected it. Shard output: each leaf returns {shard id, assigned unit ids, covered unit ids, status, entries, errors} . assigned unit ids and covered unit ids contain source unit IDs. Entries contain typed ledger items discovered in those units, each with a deterministic post extraction obligation ID or symbol key as dedup key . Never prose onl

proof-checker