Verify Sequential Statements

Verify Sequential Statements

Check each statement and subproof in order and log all local issues.

Input Contract

Assume:

• Proof is markdown text.
• The proof is written in good mathematical order.
• Statement contains the target theorem statement and its hypotheses.

Do not split the proof with utility code. Read the markdown in order and use its own structure.

Procedure

1. Extract the assumptions and hypotheses from Statement before checking the proof.
2. Iterate through the statements/subproofs in the order they appear in the markdown.
3. For each item, determine a location key:
   • use the displayed theorem/lemma/claim heading if present,
   • otherwise use a local textual locator such as proof paragraph 2.
4. Check local reasoning:
   • Is the inference valid?
   • Are assumptions stated and sufficient?
   • Is each theorem application valid in context?
   • Are there skipped or hand-wavy steps?
5. Pay special attention to assumptions that an object exists or satisfies a property — sometimes such an object has not been constructed, or it exists but has not been proved to satisfy the claimed property.
6. Audit whether the assumptions from Statement are actually used in the proof.
7. If some assumptions seem unused, do not assume they are harmless. Reason carefully about whether:
   • the assumption is truly redundant, or
   • the proof is silently omitting a necessary use of it and therefore has a gap or error.
8. Classify findings:
   • critical_error: logical contradiction, invalid theorem use, false implication.
   • gap: missing derivation, vague justification, unsupported step, or suspiciously unused assumptions whose role is not justified.
9. Also apply the Hard Prohibitions defined in the verifier contract (agents/contracts/verifier.md, "Hard Prohibitions to enforce"): P1 (citing problem.md / data/<NAME>.md as a substantive math source), P3 (an unproven conditional premise with no same-paragraph fact_id citation), P5 (a vague gesture at a "well-known"/"classical" result without a specific citation), and P6 (a statement that is not self-contained). Do not restate or fork the prohibition wording here — read and apply it from the contract so there is a single source of truth. These prohibitions are strictly additive: they only ever add findings (reject more), never remove them.
10. Keep each checked item in context for the synthesis step. You persist nothing — the verifier is stateless; the worker does all writing.

Output Contract

Produce one record per checked item, kept in context for synthesis:

{
  "location": "Lemma 3",
  "status": "checked",
  "critical_errors": [
    {"location": "Lemma 3", "issue": "Incorrect implication from A to B."}
  ],
  "gaps": [
    {"location": "Lemma 3", "issue": "Missing justification of boundedness."}
  ]
}

Tools

• None — pure reasoning over the proof; findings stay in context.