# Verify Sequential Statements

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

- Skill: `frenzymath/verify-sequential-statements-2` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add frenzymath/verify-sequential-statements-2`
- Raw SKILL.md: https://api.skillmd.com/api/skills/frenzymath/verify-sequential-statements-2/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Docs & Writing
- Author: frenzymath (https://skillmd.com/u/frenzymath)
- Updated: 2026-09-22
- Page: https://skillmd.com/skills/frenzymath/verify-sequential-statements-2

---


# 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?
   - 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?
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, 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.
9. Persist each checked item to `statement_checks` using `memory_append`.

## Output Contract

Append records to `statement_checks` with structure like:

```json
{
  "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`