Proofcheck

ProofCheck — Mathematical Proof Verification for Statistics/ML Theory Papers

🔬 Model Recommendation: Run this skill on Claude Opus for best results. Mathematical proof verification requires deep reasoning. If your session is not on Opus, run /model opus before invoking. The skill will also delegate heavy reasoning to Opus sub-agents internally when the Agent tool is used.

Systematically check proofs in long technical appendices using a structured, evidence-based methodology with multi-pass verification.

Based on: https://github.com/maweiruc/proofcheck-stat-paper

Context: $ARGUMENTS

Core Objective

Given the paper's stated assumptions, definitions, and cited results, does each claimed theorem follow with the stated constants, rates, quantifiers, probability levels, domains, and edge cases?

Goal: Find correctness issues — NOT summarize the proof. Never silently repair proofs.

Operating Principles

1. Evidence First: Every conclusion cites exact page/section/equation/line numbers. No vague references.
2. Small Proof Units: One definition, one lemma, one proof at a time. Never verify 20+ pages at once.
3. Separate Facts/Inferences/Suspicions: Verified (checked + referenced), Inferred (likely but unchecked), Suspect (possible gap).
4. No Silent Repairs: If proof proves B but claims A, record the mismatch explicitly.
5. Human Owns Final Judgment: Agent indexes, cross-checks, and reconstructs. Human reviews all S0/S1 issues.

Severity System, Verification Statuses, and Provability Triage

The S0-S3 severity system, the five verification statuses (Verified / Conditionally verified / Gap found / Incorrect / Not checked), and the three-class provability triage (PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED) are defined in ../stat-shared-references/proof-closure-machinery.md. That file is the single source of truth shared with proof-repair and proof-writer.

Operational note for this skill:

• Apply the severity system in Pass 5 (Final Report) when assigning severity to each open issue.
• Apply the provability triage at the start of each unit's deep-check (per Pass 1 Step 3, "Sketch-vs-Complete classification" + this triage).
• Set verification statuses on each unit's local check file in audit/04_local_checks/.

Proof Strategy Classification (per unit)

Identify the proof technique BEFORE step-by-step checking — different strategies have different failure modes:

Workflow

0. Setup Workspace

Parse $ARGUMENTS to locate the paper's LaTeX source file.

# Create workspace structure
PAPER_DIR="papers/$(basename "$PAPER_PATH" .tex)"
mkdir -p "$PAPER_DIR/audit"/{01_index,02_ledgers,03_dependencies,04_local_checks,05_adversarial,06_reports}

If $ARGUMENTS is a directory, look for paper.tex inside it. If it's a .tex file path, use it directly.

Detect Reference Mode (one-file vs two-file submission)

Before any cross-reference audit, detect whether the paper is:

• Mode A: single-file — one .tex compiles to one PDF (arXiv, NeurIPS/ICML)
• Mode B: two-file — paper.tex + supplement.tex (or similar) compile separately (typical for JASA, AoS, JRSS-B, Biometrika, Econometrica, JBES, JOE)

# Count top-level .tex files (excluding files that are \input by others)
find "$(dirname "$PAPER_PATH")" -maxdepth 1 -name "*.tex" -type f
# Look for explicit supplement files
ls "$(dirname "$PAPER_PATH")"/{supp*,supplement*,appendix*,SI*}.tex 2>/dev/null
# Look for S-prefix labels — strong signal of Mode B
grep -l 'label{[^}]*:S[._]\|label{S' "$(dirname "$PAPER_PATH")"/*.tex 2>/dev/null

Record in CHECK_PLAN.md:

## Reference Mode
Mode: [A: single-file / B: two-file]
Files: [list]
Cross-file convention (if Mode B): hard-coded numbers (e.g., "Lemma S.3", 
       "Theorem 2.1 of the main text") — NOT \ref{} across files

This mode affects Pass 0's cross-reference audit (Step 2B) — see below.

1. Bootstrap — Generate CHECK_PLAN.md + EXECUTION_ORDER.md

Read the paper and extract the proof architecture. Do NOT check any proofs yet — only map the terrain.

1A. Extract Proof Architecture (→ CHECK_PLAN.md Part A)

Read these sections of the LaTeX source:

1. Introduction — contributions subsection, look for TikZ dependency diagrams
2. Proof strategy section — "Proof Strategy", "Proof Outline", "Overview of Proofs"
3. Appendix structure section — the appendix's own roadmap
4. Main theorem statements

Produce:

• Core Proof Strategy (≤5 sentences): the fundamental challenge, the solution, the key innovation
• Dependency Diagram (ASCII art): reconstruct from paper's figures or theorem statements
• Critical Proof Chains (3-5 chains): base lemmas → main theorems
• Key Definitions Table: notation appearing across multiple sections

1B + 1C. Index the architecture (script)

Run the mechanical indexer instead of hand-running grep and a manual topological sort:

python ../stat-shared-references/scripts/proof_index.py \
  --main paper.tex \
  --supplement supplement.tex \
  --supplement-mode separate-self-contained \
  --json-out audit/proof_index.json \
  --md-out audit/01_index/PROOF_INDEX.md

The script is authoritative for the mechanical parts of Step 1B/1C and Pass 0 Task 2B:

• Proof unit inventory: every theorem-like environment (theorem, lemma, proposition, corollary, definition, assumption, condition, remark, claim, fact) with type, label, line, and statement summary.
• Dependency graph: for each unit's proof block, the indexed labels it \refs.
• Topological layers: a valid check order (Layer 0 = no internal deps; Layer k = deps in layers < k), with cycle detection (a dependency_cycle FAIL means the proof order is not well-founded).
• Cross-reference integrity: \ref targets with no \label (FAIL), and cross-file leaks under separate-self-contained (FAIL — the canonical two-file submission bug).
• Reference mode: single-file vs two-file detection.

Exit code 1 means at least one structural FAIL (undefined ref or dependency cycle); fix those before deep-checking. Provenance (script_version, rules_version, rules_digest) is in the report header.

What the script does NOT produce, and you still supply by judgment:

• The core proof strategy narrative (1A): the fundamental challenge, the key innovation. Read the introduction and proof-strategy section for this.
• Critical proof chains: which base lemmas feed which main theorems, and which units are load-bearing. The topological layers are the raw material; deciding the critical path is judgment.
• Per-unit assumption strength and regime (Task 2A judgment columns below).

2. Pass 0 — Indexing (Map the Terrain)

Three parallel tasks:

Task 2A: Theorem Inventory → audit/01_index/theorem_inventory.md

For each: label, exact location, mathematical objects, assumptions (explicit + inherited), claimed conclusion, probability/asymptotic regime, constants (universal vs problem-dependent), where used. If assumptions.lock.md exists, record each unit's assumptions as invoked registry IDs (A1, A3) resolved against the shared store, not as re-typed statements; an assumption in a proof with no matching registry ID is itself a finding (see Pass 3 check 3b).

Task 2B: Cross-Reference Audit — covered by the script in Step 1B/1C.

The undefined-ref and cross-file-leak checks are mechanical and are produced by proof_index.py (findings undefined_ref and cross_file_ref_leak). Read audit/01_index/PROOF_INDEX.md for them. The script auto-detects single-file vs two-file mode.

Two convention checks remain judgment and are not mechanized (the script flags the leak; you assess the phrasing fix):

• Hard-coded number convention: in two-file mode, each "of the supplement" / "of the main text" mention should be paired with a hard-coded number (e.g., "Lemma S.3 of the supplement"), since \ref cannot cross files. The script flags the broken \ref; you confirm the textual replacement reads correctly.
• Supplement numbering consistency: the supplement's theorem/equation counters should use S-prefix display numbers (e.g., \renewcommand{\thelemma}{S.\arabic{lemma}}). Verify this by inspection.

Task 2C: Notation Ledger → audit/02_ledgers/notation_ledger.md

Check for: symbols used before definition, same symbol for different objects, scalar/vector mismatch, random/deterministic mismatch, norm changes, constants with changed dependencies.

Also build:

• audit/02_ledgers/assumption_ledger.md — ID | Assumption | Location | Scope | Used by | Strength needed | Status
• audit/03_dependencies/dependency_graph.md — dependency table + circularity analysis

3. Pass 1 — Check Critical Path

Check the chain leading to the main theorem FIRST. Prioritize lemmas used by many later results.

MANDATORY first sub-step: Sketch-vs-Complete Classification

Before checking proof correctness, classify whether what the paper provides is ACTUALLY a proof, or only a sketch / outline. This is distinct from step-skipping (which is about individual missing steps within a proof) — this is about whether the entire proof body is rigorous derivation or just high-level summary.

Three-class classification:

Sketch indicators (any combination triggers PARTIAL-SKETCH or SKETCH-ONLY):

• Title or section explicitly says "Proof Sketch" / "Sketch of Proof" / "Outline of Proof"
• Body contains: "We sketch the proof", "Full details in the supplement", "Detailed proof is omitted"
• Proof length disproportionate to claim complexity (e.g., 5 lines for a 2-page theorem)
• Body is purely verbal narrative ("we first bound X using Y, then apply Z") with no derived equations
• "Similar to / follows from [Paper Z]" without showing the adaptation
• Heavy use of "it can be shown that" / "by standard arguments" / "after some algebra"
• "We omit the details for space"
• Technical core deferred entirely: "Lemma N is proved in Appendix X" but Appendix X is also sketch-only
• A theorem whose proof is a single paragraph + a citation to another paper

Crucially: a proof labeled "Proof Sketch" is NOT a sufficient verification of the claim. If the paper relies on this sketch as evidence for the theorem, the theorem's actual status is at best CONDITIONALLY VERIFIED pending the full proof. Reviewers at AoS / JASA / JRSS-B / Biometrika do not accept main-text sketches without full proofs in supplement.

Record in the unit check file:

### Sketch-vs-Complete Audit
- Class: [COMPLETE / PARTIAL-SKETCH / SKETCH-ONLY]
- Sketch indicators found: [list specific evidence]
- For PARTIAL-SKETCH: each gap recorded as an S1 issue requiring expansion
- For SKETCH-ONLY: STATUS is forced to "SKETCH-ONLY — NO PROOF PROVIDED"
- Supplement location (if proof is supposed to be elsewhere): [pointer + verify it IS complete there]
- **Expansion status**: [REQUIRED / IN-PROGRESS / COMPLETED] ← MANDATORY field
- **Expanded proof file**: [path, set once expansion is complete]

If the "real" proof is supposed to be in supplementary material, follow the link and audit the supplement proof; if the supplement proof is also a sketch, both get tagged SKETCH-ONLY.

HARD RULE: detection requires immediate expansion

A sketch detected during /proofcheck cannot remain unexpanded in the final audit output. The audit is NOT complete while sketches remain.

When SKETCH-ONLY or PARTIAL-SKETCH is found:

1. Mark the unit with Expansion status: REQUIRED
2. Immediately hand off to /proof-repair (Expand-Sketch-to-Proof repair class) which then invokes /proof-writer for the actual writing
3. /proof-writer must produce either:
   • A COMPLETE proof (Expansion status → COMPLETED)
   • An explicit NOT-CURRENTLY-JUSTIFIED blockage report (then the theorem itself is downgraded; the sketch is still removed)
4. After expansion, re-run the Sketch-vs-Complete classification on the new proof body — verify it now classifies as COMPLETE
5. The audit is blocked from "Pass 5: Final Report" until every detected sketch has Expansion status of either COMPLETED or BLOCKAGE-REPORT-WRITTEN

The Final Report's executive summary MUST contain a row:

Sketches detected: N
├── Expanded to complete proof: M
├── Determined to be unprovable as stated (blockage report): K
└── Outstanding (NOT ALLOWED in final state): 0

If any sketch remains in "REQUIRED" or "IN-PROGRESS" state when the audit attempts to finalize, the skill REFUSES to mark the audit complete and returns to expansion.

For EACH proof unit, create one file: audit/04_local_checks/section_X/{ID}_{name}_check.md

Each file follows this template:

## Proof Unit: [ID / Name]
- Location:
- Type: [definition / lemma / proposition / theorem / proof segment]
- **Sketch class**: [COMPLETE / PARTIAL-SKETCH / SKETCH-ONLY]   ← from Sketch-vs-Complete audit
- Proof Strategy: [direct / contradiction / induction / construction / reduction / coupling / optimization / epsilon-delta]
- Provability: [PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED]
- Status:
- Confidence:

### Claim Normalization
**Original statement**: [exact copy from paper]
**Normalized form**: [rewritten with all quantifiers, domains, types explicit]
**Interpretation notes**: [any ambiguity resolved, notation clarified]

If the normalized form is stronger/different from the original, flag this explicitly.

### Explicit Assumptions
- [Assumption 1]

### Inherited / Implicit Assumptions
- [Standing assumption]
- [Hidden assumption detected: ...]

### Dependencies
| Dependency | Location | Required form | Available? | Verified? | Notes |
|------------|----------|---------------|------------|-----------|-------|

### Step-by-Step Verification
| Step | Location | Claim | Justification | Verdict | Notes |
|------|----------|-------|---------------|---------|-------|
| 1 | Eq.(42)→(43) | Triangle ineq | Same norm | Valid | None |
| 2 | Eq.(43)→(44) | Lemma A.2 | Needs boundedness | Gap | Missing assumption |

**Anti-fabrication checklist** — flag ANY instance of:
- "clearly" / "obviously" / "it is easy to see" hiding a nontrivial step
- "by standard arguments" without specifying WHICH standard argument
- "similarly" referring to a non-analogous situation
- A step justified only by "by the above" without exact reference
- Unmarked use of a stronger assumption than what is stated

### Edge Cases & Boundary Analysis
- [Boundary case checked: what happens when parameter = 0/1/∞?]
- [Degenerate case: what if matrix is singular / set is empty / dimension = 1?]
- [Domain boundary: does the result hold at the boundary of Θ?]

### Issues
| Severity | Confidence | Description | Evidence | Proposed repair |

### Final Verdict
[Verified / Conditionally verified / Gap found / Incorrect / Unclear]

### If Gap Found: Blockage Report
- **Exact blocker**: [which step fails and why]
- **What would fix it**: [minimal extra assumption / lemma / technique needed]
- **Weaker claim that IS provable**: [if applicable]
- **Candidate literature**: [known results that might bridge the gap — to be expanded by /proof-repair]

Key checks for each step:

• Every equation transition and inequality direction
• Every quantifier and probability statement
• Every constant, rate, domain, dimension
• Every boundary case
• Conclusion vs. statement match
• Conclusion matches EXACTLY what was proved (not a stronger restatement)
• Every nontrivial implication is justified — no "clearly" or "obviously" allowed

Step Completeness Audit (sub-step within each unit check)

This audit is mandatory for every proof unit. Going beyond passive anti-fabrication word-flagging, it ACTIVELY identifies step jumps and reconstructs them.

A. Skip-point detection

For each proof unit, scan for skip indicators in three categories:

Category 1: Verbal skip phrases

• "clearly" / "obviously" / "it is easy to see" / "trivially"
• "by standard arguments" / "as is well-known" / "it is well-known"
• "after some algebra" / "after simplification" / "by direct calculation"
• "by symmetry" / "similarly" / "the same argument applies"
• "the rest follows" / "the conclusion is now immediate" / "we omit the details"
• "as before" / "by the above" / "in an analogous manner"

Category 2: Equation-number jumps

• Eq.(k) appears, then Eq.(k+m) for m ≥ 2 without intermediate equations
• A displayed equation followed by ≥2 lines of unjustified manipulation
• Use of an unstated identity to transform one expression to another

Category 3: Implicit logical jumps

• A conclusion drawn from a previous claim without stating the inference rule
• A bound used as both upper and lower without separate justification
• An optimization step where existence of optimizer is assumed but not shown
• A limit/sum/integral exchanged without naming the convergence theorem

B. Reconstruction attempt

For EACH detected skip, attempt to fill in the missing steps:

1. List what is being claimed before the skip (the input state)
2. List what is being claimed after the skip (the output state)
3. Reconstruct the bridging steps explicitly (using paper assumptions + cited results + standard mathematical facts only — no fabrication)
4. Count the reconstructed steps and assess the techniques used

C. Skip classification (for each detected skip)

Based on the reconstruction:

D. Step Completeness Table (per unit)

Add to each unit's check file:

### Step Completeness Audit

| Skip # | Location | Skip indicator | Input state | Output state | Reconstruction | Class | Severity |
|--------|----------|---------------|-------------|--------------|----------------|-------|----------|
| 1 | Line 152, "obviously" | verbal | f(x) ≥ 0 ∀x | ∫f dμ ≥ 0 | Apply monotonicity of integral (1 line) | TRIVIAL | — |
| 2 | Eq.(47)→(50) | equation jump | LHS of (47) | RHS of (50) | Algebraic expansion + Cauchy-Schwarz + bound on ‖∇f‖ (4 lines) | VERIFIABLE | S3 |
| 3 | "by symmetry" line 198 | verbal | Bound on E[XY] | Bound on E[X²]+E[Y²] | Symmetry NOT applicable here — X,Y not exchangeable | NONTRIVIAL | S1 |
| 4 | "after some algebra" line 220 | verbal | Eq.(60) | Eq.(61) | Cannot reconstruct — requires unstated identity for matrix inverse | UNRECONSTRUCTIBLE | S0 |

**Summary**: 4 skips found. 1 trivial, 1 verifiable, 1 nontrivial (S1), 1 unreconstructible (S0).

E. Reconstruction discipline (anti-fabrication for the checker)

When reconstructing steps, the checker itself must follow rigor rules:

• Use ONLY: paper's stated assumptions + cited results + named standard facts (e.g., Cauchy-Schwarz, Jensen, triangle inequality, Holder's)
• For named standard facts, cite the name explicitly ("by Cauchy-Schwarz")
• Do NOT invent intermediate inequalities or unstated lemmas
• If a reconstruction requires invoking a non-obvious lemma, classify as NONTRIVIAL and record what lemma is needed
• If reconstruction succeeds but uses techniques not in the paper's framework (e.g., heavy machinery from a different subfield), flag as suspect — the author probably intended a simpler bridge that we're missing

4. Pass 2 — Check Support Lemmas

After critical path confirmed, check remaining lemmas in parallel within each phase. Same per-unit template as Pass 1.

Also maintain:

• audit/02_ledgers/constants_ledger.md — track which constants are universal vs problem-dependent
• Event ledger — track probability events, their definitions, and how they compose

5. Pass 3 — Global Consistency

Cross-cutting checks after all local checks:

1. No circular dependencies — trace every chain to base assumptions
2. Notation consistent — no symbol drift between sections
3. Assumptions propagate — every cited assumption is in scope where used 3b. Shared assumption store (if assumptions.lock.md exists; schema in ../stat-shared-references/assumptions-lock-protocol.md) — resolve every theorem's invoked assumption IDs against the registry and run consistency triage, not satisfiability certification. Flag: (i) an assumption stated in a proof that is not a registry ID (unregistered — should be invoked or appended); (ii) two near-duplicate registry rows that are the same assumption under different short names (should be one ID); (iii) a theorem co-invoking IDs marked incompatible-with each other or two variant-of the same base; (iv) invoked-but-unused IDs (minimality — a theorem carrying an assumption its proof never consumes, which weakens its stated generality). Expand any profile alias (P-base = {A1,A2,A3}) before the unused check. Emit PASS: no direct contradiction found / FLAG: axis tension / FAIL: direct contradiction / UNKNOWN: common model not certified — never claim the full registry is jointly satisfiable (a framework may hold mutually exclusive regimes on purpose). Write findings to audit/03_dependencies/assumption_lock_triage.md.
4. Theorems assemble — each main theorem's transitive dependencies all proved
5. Quantifier consistency — check "for all ∃" vs "∃ for all", uniform vs pointwise, parameter-dependent vs universal constants
6. Probability/event consistency — events defined? Intersections handled? Failure probability accumulated correctly?
7. Constants/rates consistency — are O(·) terms hiding forbidden dependencies? Rates preserve all n, d, δ, ε?
8. Asymptotic-order consistency / negligibility closure — every disappearing term must have a recorded comparison scale and a recorded bridge. For each proof unit, build a local dropped-term ledger with columns Term dropped | Needed scale | Support source | Bridge | Verdict, where Support source is one of local bound, earlier proved lemma, or audited citation, and Bridge is the explicit calculation or one-line mode conversion that turns that support into the claimed o(·) / o_p(·) / negligible / dominated conclusion. Deterministic order arithmetic may pass trivially, but any uniformity, conditioning, dependence, Taylor-remainder, or parameter-dependent-constant claim requires an explicit derivation. If a unit drops a term without a filled bridge entry, proves only the wrong scale, or upgrades pointwise or on-event control to uniform or unconditional negligibility without justification, flag.

For the asymptotic-order check, each local check file should expose the bridge in a compact table:

### Dropped-Term / Negligibility Ledger
| Term dropped | Needed scale | Support source | Bridge | Verdict |
|--------------|--------------|----------------|--------|---------|

A missing row, wrong comparison scale, unsupported dominance claim, or unjustified pointwise-to-uniform / on-event-to-unconditional upgrade is a Global Consistency flag. See the Trap Catalogue item #9 and the Negligibility-Closure Trivial-Pass Tier in ../stat-shared-references/proof-strategy.md for the discriminator between Tier-1 (deterministic order arithmetic, free pass), Tier-2 (stochastic mode conversion, one-line bridge), and Tier-3 (uniformity / conditioning / dependence / Taylor / parameter-dependent constants, explicit derivation required).

6. Pass 4 — Adversarial Review

Deliberately try to break the proof:

Counterexample search: What happens with d=1, n=1, zero variance, singular matrix, boundary of parameter space, heavy tails, equal parameters, probability-zero events, flat/non-smooth functions?

Hidden assumption search: For each proof unit check:

• Division by zero? Matrix invertibility without proof?
• Limit/expectation/derivative/integral exchange without justification?
• Concentration without independence/tail checks?
• Compactness without compact domain?
• Minimizer existence assumed? Uniqueness used but not proved?
• High-probability statements used simultaneously without union bound?
• Uniform result claimed from pointwise proof?

External theorem misuse: Check exact prerequisites, finite-sample vs asymptotic, pointwise vs uniform, matching notation.

Stress assumptions: Remove each assumption → which step fails? Does proof use stronger version than stated? Are there unused assumptions?

Assumption load-bearing audit: For each load-bearing assumption (one a main theorem's critical chain actually consumes — skip unused/purely-technical conditions, which the "unused assumption" check above already covers), apply the four tests in ../stat-shared-references/assumption-loadbearing-audit.md: T1 Conclusion Restatement (S0, merges with the circularity gate), T2 Verification Target Assumed (S1), T3 Central Difficulty Pre-emption (S1, capped — escalates to S0 only as a vacuous-class / OVERSTATED statement-scope / silent-downstream defect), T4 Comparative Axis Reversal (S1 headline / S2 local). This needs the introduction's claimed central difficulty and the Task 2A inventory, not just the local proof — that is why it lives in Pass 4, not Pass 2. Absence of a finding is the expected result for a clean conditional theorem; proof length is never evidence. For any flagged assumption, produce the Original Assumption Challenge Ledger from that reference and route by repair type (T1 → proof-repair; relaxable T2/T3/T4 → theory-sharpen; oversold-but-correct → stat-polishing).

Write findings to audit/05_adversarial/hidden_assumptions.md and audit/05_adversarial/counterexamples.md. Put any load-bearing-audit findings and the Challenge Ledger in audit/05_adversarial/assumption_loadbearing.md.

Codex Adversarial Cross-Review (if Codex MCP available)

Follow ../stat-shared-references/codex-protocol.md — Codex is an adversarial reviewer to discuss with iteratively, not an oracle to defer to. Every Codex finding requires explicit ACCEPT / PUSH BACK / REQUEST CLARIFICATION with reasoning. Forbidden behaviors: silent wholesale acceptance, silent rejection, agreement without recording why. The skill must emit codex_discussion.md documenting the full round-by-round dialogue.

Use mcp__codex__codex to get an independent second opinion from a different model. The key design: Codex does NOT see Claude's findings — it forms its own judgment first.

For each S0/S1 issue found by Claude, send to Codex:

mcp__codex__codex:
  config: {"model_reasoning_effort": "high"}
  prompt: |
    You are an adversarial reviewer of mathematical proofs in statistics/ML theory.

    Here is a proof unit from a paper:
    [Paste: lemma statement + proof text + assumptions + dependencies]

    Claude (another AI) claims this proof has a SPECIFIC issue:
    [Paste: issue description, severity, evidence]

    Your tasks:
    1. INDEPENDENTLY verify: do you agree this is a genuine issue?
       - If YES: confirm and rate severity (S0 fatal / S1 major / S2 moderate / S3 minor)
       - If NO: explain why Claude's concern is invalid or overstated
    2. Find issues Claude MISSED: are there other problems in this proof unit?
    3. For each genuine issue: is there an obvious fix?

    Rules:
    - Cite exact equations, line references, or proof steps
    - Do not fabricate issues — "no additional issues found" is a valid answer
    - Be precise about severity: S0 means the main theorem breaks, not just a local gap

For each unit Claude marked "Verified", spot-check 20-30% via Codex:

mcp__codex__codex:
  config: {"model_reasoning_effort": "high"}
  prompt: |
    You are checking a mathematical proof for correctness.

    Here is a proof unit:
    [Paste: lemma statement + proof text + assumptions]

    Another reviewer marked this as "Verified — no issues."
    Your job: try to BREAK this verdict. Look for:
    - Hidden assumptions not listed
    - Inequality direction errors
    - Quantifier mistakes (pointwise vs uniform)
    - Missing edge cases
    - External theorems used outside their conditions

    If you find a genuine issue, describe it with severity and evidence.
    If the proof is indeed correct, say "Confirmed: no issues found" and briefly explain
    why the key steps are valid.

Reconciliation: After Codex responds, classify each finding:

Write reconciliation to audit/05_adversarial/codex_cross_review.md.

7. Pass 5 — Final Report

Every generated artifact begins with the Artifact Manifest Header described in ../stat-shared-references/codex-protocol.md. The manifest lets downstream skills (proof-repair, --post-repair, theory-sharpen) load only what they need and detect staleness against the paper's current state.

Write audit/06_reports/FINAL_REPORT.md:

---
artifact: audit_final_report
scope: global
source_files: [paper.tex, supplement.tex if Mode B]
theorem_ids: [every theorem / lemma / proposition / corollary in the inventory]
assumption_ids: [every assumption in the assumption ledger]
issue_ids: [every issue in issue_log.md]
commit: [paper-repo short SHA at audit time, or content hash if not in git]
generated: [YYYY-MM-DD HH:MM]
generator: proofcheck v1.7.0 Pass 5
---

# Final Proof-Check Report: [Paper]

## Executive Summary
- Overall verdict:
- Main theorem support:
- Highest severity issue:
- Checked units: X / Y total
- Open issues: N (S0: _, S1: _, S2: _, S3: _)

## Checked Scope
- Sections checked:
- Results checked:
- Results NOT checked:

## Main Dependency Chain
[How main theorem depends on intermediate results]

## Verified Results
| Result | Status | Confidence | Notes |

## Open Issues (ranked by severity)
| ID | Severity | Confidence | Affected result | Summary |

## Conditional Results
| Result | Condition needed | Evidence |

## Recommended Repairs
1. [Repair]

## Final Judgment
[Correct / Correct modulo repairs / Incomplete / Incorrect]

Also write audit/06_reports/issue_log.md with all issues. Same manifest header (artifact: issue_log, scope: global).

Per-unit local check files in audit/04_local_checks/section_*/ carry their own manifest with scope: local, theorem_ids: [single unit being checked], and assumption_ids: [assumptions used in that unit's proof]. This lets downstream calls (and re-audit) skip loading the full FINAL_REPORT.md when they only need one unit's verdict.

audit/08_post_repair/RE-AUDIT_REPORT.md and audit/08_post_repair/diff_ledger.md likewise begin with manifest headers; their scope is usually dependency_expanded (the touched units plus their dependencies) and their commit field records the paper-repo SHA at re-audit time, allowing downstream consumers to detect whether the re-audit is fresh.

Common Failure Patterns (Diagnostic Checklist)

Logical

• Proving weaker statement than claimed
• Assuming the conclusion / circular dependency
• Missing induction base case
• Existence without compactness/coercivity
• Uniqueness used but not proved

Quantifier

• Pointwise result used as uniform
• Parameter-dependent constant claimed universal
• "∀ε ∃N" confused with "∃N ∀ε"
• High-prob for fixed object used over class without covering

Probability

• Missing independence
• Conditional probability mishandled
• Event intersection not adjusted
• Expectation bound used as high-prob bound
• Random index in fixed-index concentration

Analysis

• Limit/expectation exchanged without DCT/MCT/UI
• Derivative/integral exchanged without regularity
• Compactness assumed but not stated

Algebra & Inequality

• Wrong inequality direction
• Dropping absolute value
• E[XY] = E[X]E[Y] without independence
• Jensen in wrong direction
• Operator/Frobenius/vector norm confused

Asymptotic & Rate

• O_P used as deterministic O
• Constants in O(·) depend on n
• Dimension/log factors dropped
• Finite-sample theorem proved only asymptotically

Citation

• External theorem requires stronger assumptions
• External theorem conclusion weaker than needed
• Asymptotic theorem used for finite sample

Paper-Type Adaptations

Asymptotic Theory

• Check o_P, O_P, o, O usage correctness
• Verify CLT/Lindeberg conditions
• Watch uniform vs pointwise convergence

Concentration Inequalities

• Check tail conditions (sub-Gaussian, sub-exponential, bounded moment)
• Verify union bounds over infinite classes
• Check δ (failure probability) propagation

Optimization Theory

• Check convexity/smoothness assumptions
• Verify minima exist (compactness + continuity)
• Watch local vs global optimum confusion

Markov Chain Theory

• Check drift conditions uniform over parameter space
• Verify small set conditions simultaneous (not pointwise)
• Watch geometric vs plain ergodicity

M-Estimation

• Check identifiability (unique maximizer)
• Verify score function mean zero
• Check Hessian invertibility

Quick-Start Mode

If time is limited, do the minimal version:

1. Build theorem/lemma inventory
2. Identify main theorem's dependency chain
3. Check final theorem proof
4. Check each direct dependency
5. Track assumptions + notation while checking
6. Run hidden-assumption search on main chain
7. Run constants/rates check on main chain
8. Produce issue log with severity
9. State final confidence + unchecked scope

Session Management

After each checking session, update PROGRESS.md:

## Session Summary: [Date]
- Proof units checked:
- New verified results:
- New issues:
- Updated dependencies:
- Open blockers:
- Next targets:

Pipeline Integration

This skill is part of a 3-skill pipeline:

/proofcheck → /proof-repair → /proofcheck --post-repair → /proof-writer
  Find issues    Fix + literature    Convergence test         Write complete proofs

• Blockage reports in local checks feed directly into /proof-repair Step 1 (Issue Triage)
• Candidate literature hints in blockage reports give /proof-repair a head start on search
• Provability triage (PROVABLE AFTER WEAKENING) tells /proof-repair to use Weaken-Claim class
• After /proof-repair designs a fix, /proof-writer writes the complete corrected proof
• After patches are applied, /proofcheck --post-repair performs the convergence test (see Post-Repair Re-Audit Mode below)

To run the full pipeline:

/proofcheck papers/my-paper/paper.tex          # Step 1: find all issues (full 6-pass audit)
/proof-repair papers/my-paper/                 # Step 2: design repairs + find literature
/proofcheck --post-repair papers/my-paper/     # Step 2.5: convergence test (delta audit)
/proof-writer [specific claim to rewrite]      # Step 3: write corrected proof text

Post-Repair Re-Audit Mode (--post-repair)

Invoked as /proofcheck --post-repair papers/<paper-name>/. This is a focused delta audit, not a full 6-pass re-run. The goal is to verify that /proof-repair's output actually converged: every originally flagged issue is closed, no new fatal/major issue was introduced by the patches, and the global consistency of assumptions and dependencies still holds.

When to invoke

• Always after /proof-repair finishes a plan that touches any S0 or S1 issue. This is a HARD GATE: /proof-repair cannot mark REPAIR_PLAN.md complete until this mode has run and reports CONVERGED.
• Strongly recommended (not gated) after /proof-repair on S2/S3-only plans, because patches can still introduce silent regressions even when they target minor issues.
• After applying any human-authored patch to a paper that already has an audit/ directory, to verify the manual edit did not break a downstream proof.
• After stat-polishing --formal-statement-pass produces an EQUIVALENCE_LEDGER.md row whose proofcheck status is "required (on main chain)". A formalized assumption or statement on the dependency path to a headline theorem, rate theorem, or main-chain lemma is a semantic edit and gets the same re-audit as a proof-repair semantic edit. The ledger row is the entry point: its "touched axis" and "downstream consumers" columns scope the affected sub-DAG. See ../stat-shared-references/equivalence-ledger-protocol.md for the proofcheck depth split (targeted dependency check for off-chain rewrites; full --post-repair for on-chain).

Inputs

The mode reads, in order:

1. The original audit at papers/<paper-name>/audit/ — especially 06_reports/FINAL_REPORT.md, 06_reports/issue_log.md, 02_ledgers/{notation,assumption,constants}_ledger.md, and 03_dependencies/dependency_graph.md.
2. papers/<paper-name>/REPAIR_PLAN.md — the

…(truncated)