proof-checker

What it does

Rigorous mathematical proof verification and fixing workflow. Reads a LaTeX proof, identifies gaps via cross-model review, fixes each gap with full derivations, re-reviews, and generates an audit report. Use when user asks for rigorous mathematical verification of a theory paper.

How it works

• Phase 0: Preparation
  • Locate the main .tex file(s) and read the entire proof to build a section map with line numbers and key claims.
  • Read reference materials and identify the main theorem, its assumptions, and claims.
• Phase 0.5: Proof-Obligation Ledger
  • Create artifacts saved to PROOF_SKELETON.md, including Dependency DAG, Assumption Ledger, Typed Symbol Table, Canonical Quantified Statements, Micro-Claim Inventory, and Limit-Order Map.
• Phase 1: First Review (Codex GPT-5.4 xhigh)
  • Submit complete proof content with a mandatory checklist covering definitions, hypothesis discharge, inequality audit, interchange audit, probability mode, uniformity, edge cases, and dependency consistency.
  • Output per-issue fields: id, status, impact, category, location, statement, why_invalid, counterexample, affects, minimal_fix.
  • Save results to PROOF_AUDIT.md as the reviewer’s issue list.
• Phase 1.5: Counterexample Red Team
  • For CRITICAL/MAJOR issues and key lemmas, attempt to construct counterexamples using strategies like dimensional collapse, degeneracy, extremal distributions, adversarial parameter scaling, and numeric falsification. Log attempts in PROOF_AUDIT.md.
• Phase 2: Fix Implementation
  • For each issue, choose a fix strategy (ADD_DERIVATION, STRENGTHEN_ASSUMPTION, WEAKEN_CLAIM, ADD_REFERENCE).
  • Derive the fix mathematically, possibly introducing new lemmas written in a theorem-proof style.
  • Implement changes in the LaTeX file, preserving labels.
  • Record the fix with a detailed log (Fix N: [SHORT TITLE]), including before/after, rationale, key equations, and downstream effects.
  • Run a compile check (pdflatex) to surface errors or warnings.
• Phase 3: Re-Review (Codex GPT-5.4 xhigh)
  • Run a new reviewer instance with the same mandatory checklist, verifying acceptance gates (no fatal/critical issues, justified proofs, etc.).
• Phase 3.5: Global Closure & Independent Verification
  • Ensure statement–conclusion alignment, all obligations discharged, case coverage, induction correctness (if applicable), and that any strengthened assumptions propagate properly.
  • For any FATAL/CRITICAL fixes, perform an independent second review on the fixed section.

When to use it

Use when a user requests rigorous mathematical verification of a theory paper, or when the workflow requires formal proof obligation tracking, cross-model review, and an audit trail (PROOF_AUDIT.md, PROOF_SKELETON.md, PROOF_CHECK_STATE.json). The process is configured to render the audit to HTML by default and to maintain a recovery STATE_FILE.

What it can touch

• Tools: Bash, Read, Grep, Glob, Write, Edit are declared as allowed tools. The workflow references commands like pdflatex for compilation.
• Artifacts: PROOF_AUDIT.md, PROOF_SKELETON.md, PROOF_CHECK_STATE.json, proof_audit_report.tex, and auxiliary sections for Dependency DAG, Assumption Ledger, and Micro-Claim Inventory.

Caveats

• Acceptance requires zero open FATAL or CRITICAL issues and explicit justification for all hypotheses and interchanges.
• Render_HTML is enabled by default to render PROOF_AUDIT.md to HTML, with non-blocking failures allowed.
• The process relies on external reviewer models and may be constrained by their capabilities and configurations.