proof-checker

name proof-checker description 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 check", "审证明", "check this proof", or wants rigorous mathematical verification of a theory paper. argument-hint [path-to-tex-file or proof-description] [--deep-fix] [--restatement-check] allowed-tools Bash(*), Read, Grep, Glob, Write, Edit, Agent, mcp__codex__codex, mcp__codex__codex-reply, mcp__manual_review__review, mcp__manual_review__review_reply 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 . 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": " ", "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": " ", "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: Zero open FATAL or CRITICAL issues Every theorem/lemma has: (i) explicit hypotheses, (ii) proof with all interchanges justified, (iii) every application discharges hypotheses in the ledger All big-O/Θ/o statements have declared parameter dependence and uniformity scope 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 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 Locate the proof : Find the main .tex file(s). Read the entire proof : Extract list of all theorems/lemmas/propositions/corollaries/definitions/assumptions. Read reference materials : Reference papers, prior results. Build a section map : Structured list with line numbers and key claims. 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 . Two hard rules: 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 — 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 ): 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). 2. Assumption Ledger For each theorem/lemma, list every hypothesis with WHERE each is verified — i.e. the location pointer the paper claims discharges it ( file:line ), not a judgment that the discharge is valid; mark "UNVERIFIED" when the paper cites no discharge location (not when you believe the math fails — that is the jury's call). Track usage-minimal assumption sets — which assumptions were actually used vs merely stated. 3. Typed Symbol Table Each symbol must have a type signature : κ : scalar ∈ (0,1), depends on (d, α_t, Σ, μ) u* : vector ∈ ℝ^d, u* = C^{-1}m B^even : matrix ∈ ℝ^{(L+1)×(L+1)}, symmetric PSD Ψ_v : function ℝ → ℝ, analytic in (ζ,κ), parity determined by v Flag any symbol whose meaning changes or whose type is inconsistent across uses. 4. Canonical Quantified Statements For each theorem/lemma, rewrite the statement with explicit quantifiers, domains, and limit order : ∀K ≥ 3, ∀π ∈ Π_K^{ms,∘} \ E_K, ∃κ_0 > 0 such that ∀κ ∈ (0, κ_0): h_act^{(K,π)} = Θ(κ^{α_K^act}) [uniform in π on compact subsets] If you cannot restate a theorem this precisely, mark it UNCLEAR — needs disambiguation . 5. Micro-Claim Inventory Every nontrivial step becomes a numbered micro-claim in sequent form :