verify-sequential-statements

name	verify-sequential-statements
description	Verify a markdown proof in the order it is written. Use when the task is to check local correctness, theorem applicability, and reasoning gaps statement by statement through a paper-style proof.

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. Audit whether the assumptions from Statement are actually used in the proof.
6. 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.
7. 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.
8. Persist each checked item to statement_checks using memory_append.

Output Contract

Append records to statement_checks with structure like:

{
  "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."}
  ]
}

MCP Tools

• memory_append
• memory_query