proof-checker

What it does

Rigorous mathematical proof verification and fixing workflow. Reads a LaTeX proof, identifies gaps via cross-model review (external reviewer backend, xhigh 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.

How it works

Phase 0 describes locating and reading the proof, building a section map, and identifying the main theorem. Phase 0.5 builds a proof-obligation ledger in parallel using a tiered approach: Phase 1 (Tier 1) extracts symbols/claims per section; Phase 2 (Tier 2) processes shards via subagents; Phase 3 (Tier 3) walks sections sequentially. The system enforces that shards merely extract obligations and do not adjudicate validity. The artifact outputs include a PROOF_SKELETON.md with a Dependency DAG, Assumption Ledger, Typed Symbol Table, Canonical Quantified Statements, and Micro-Claim Inventory, plus a PROOF_AUDIT.md audit, a proof_audit_report.tex, and a PROOF_CHECK_STATE.json for recovery. Render HTML of PROOF_AUDIT.md at the end when RENDER_HTML is true. The workflow uses a cross-model reviewer (CODEx backend by default) to perform an adversarial review, with memory preservation across rounds via codex-reply or manual equivalents.

Phase 1: First Review (reviewer backend, xhigh reasoning) requires submitting the complete proof content with a checklist that includes mandatory checks: A. DEFINITIONS, B. HYPOTHESIS DISCHARGE, C. INEQUALITY AUDIT, D. INTERCHANGE AUDIT, E. PROBABILITY MODE. The system uses tool calls like mcp__codex__codex or mcp__manual_review__review depending on backend, with config: {"model_reasoning_effort": "xhigh"}.

Phase 2 and beyond perform iterative reviews, fix gaps with full derivations, re-review, and update audit artifacts until convergence. The final audit report and state file reflect what was verified and where gaps remain.

When to use it

Use when the user requests rigorous mathematical verification of a theory paper or asks to check a proof in various supported phrases (Chinese and English) indicating proof verification or checking.

What it can touch

The workflow references the following artifacts and tools: PROOF_AUDIT.md, proof_audit_report.tex, PROOF_CHECK_STATE.json, PROOF_SKELETON.md, mcp__codex__codex, mcp__codex__codex-reply, mcp__manual_review__review, mcp__manual_review__review_reply. The CLAIMS extraction and cross-model review process touch these artifacts through the verifier and reviewer backends. Render HTML of PROOF_AUDIT.md at workflow end if RENDER_HTML = true.

Caveats

Acceptance requires zero open FATAL or CRITICAL issues, explicit hypothesis discharge in each theorem/lemma, and proper handling of limit orders and uniformity; counterexample checks are performed as part of audit. The process uses backends that may be Claude-vs-non-Claude in routing; the default reviewer backend is codex. If manual reviewer is unavailable, installation should print the install command and not fall back to Codex. Render HTML rendering depends on the render flag and Codex audit fidelity checks.