/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(aris-fanout-leaf), mcp__codex__codex, mcp__codex__codex-reply, mcp__manual_review__review, mcp__manual_review__review_reply, Skill(lean-formalize), mcp__antigravity__antigravity, mcp__antigravity__antigravity-reply, mcp__grok__grok, mcp__grok__grok-reply, mcp__claude-review__review, mcp__claude-review__review_reply, mcp__claude-review__review_start, mcp__claude-review__review_reply_start, mcp__claude-review__review_status

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_ASS