frenzymath/rethlas/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.

1. 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?
• Do similar-looking definitions actually match exactly?
• Do similar-looking formulas in those definitions differ in a way that matters for the argument?
• If the proof deduces one property from another, do the exact definitions and defining formulas of those two properties really support that deduction?
• For each small deduction step, do all assumptions needed for that step actually hold?

1. 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.
2. Audit whether the assumptions from Statement are actually used in the proof.
3. 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.

1. Classify findings:

• critical_error: logical contradiction, invalid theorem use, false implication.
• gap: missing derivation, vague justification, unsupported step, unjustified existence or property assumptions about objects, suspiciously unused assumptions whose role is not justified, failure to distinguish between similar-looking definitions or formulas, or a hand-wavy deduction from one property to another.

1. 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