proof-checker skill

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

• MAXREVIEWROUNDS = 3
• REVIEWERMODEL = 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).
• REVIEWERBACKEND = 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 REVIEWERBACKEND = codex: Use mcpcodexcodex for new review threads (model: gpt-6-astra, config: {"modelreasoningeffort": "ultra"}). Use mcpcodex__codex-reply for follow-up rounds (reuse threadId).

If REVIEWERBACKEND = manual: Use mcpmanualreviewreview for new review threads with: prompt: [exact same prompt that would go to Codex] config: {"modelreasoningeffort": "xhigh", "executormodel": "", "requirereviewermodel": true} Save the returned threadId. Use mcpmanualreviewreviewreply for follow-up rounds with: threadId: [saved manual-review threadId] prompt: [follow-up prompt] config: {"modelreasoningeffort": "xhigh", "executormodel": "", "requirereviewermodel": true}

Prompt fidelity: the manual prompt must be exactly the same text that Codex would receive. Review tracing applies equally to both backends.

• AUDITDOC: PROOFAUDIT.md at the paper directory root, alongside main.tex (cumulative log; when invoked via /paper-writing, this is paper/PROOF_AUDIT.md)
• REPORTTEX: proofaudit_report.tex (formal before/after PDF)
• STATEFILE: PROOFCHECK_STATE.json (for recovery)
• SKELETONDOC: PROOFSKELETON.md (micro-claim inventory)
• RENDERHTML = true — When true (default), auto-render PROOFAUDIT.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

Group B: Analysis & Measure Theory

Group C: Model & Parameter Tracking

Group D: Scope & Claims

Two-Axis Severity System

Axis A — Proof Status (what is wrong)

Axis B — Impact (how much breaks)

Severity Labels (derived)

Side-Condition Checklists for Common Theorems

When the proof invokes any of the following, require explicit verification of ALL listed conditions:

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.

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

— 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