proofreader

Compare Proofreader audit outcomes between two versions of a paper. Shows what was fixed, what regressed, what's new, and what's unchanged -- useful for revision rounds, before/after responding to reviewers, or tracking convergence across drafts.

End-to-end Proofreader pass on a paper. Evaluates, audits flagged proofs (one per result), hunts counterexamples in fresh subagents, stress-tests findings via fresh defender + arbiter subagents, and writes the results into a structured report directory.

Dispatches a fresh defender subagent and a fresh arbiter subagent to stress-test an audit finding. Each runs in isolated context for genuine independence — defender doesn't know about the arbiter, arbiter wasn't involved in producing the defense.

Independent adjudicator for an audit-vs-defense dispute over a formal result. Spawn as a fresh subagent after both `audit-proof` and `defend-finding` have produced their outputs. The agent has no stake in either side, reads the paper independently, and renders a true/false-positive verdict with a flaw taxonomy. Returns a structured Markdown report.

Author-perspective defense of a paper against a proof-audit finding. Spawn as a fresh subagent so the defense is built independently of the eventual arbiter — and so the defender has no incentive to soften its arguments in anticipation of being rebutted. Returns a structured Markdown defense. Use immediately before `arbitrate-finding` whenever an audit (and optional counterexample) needs adversarial review.

Agentic counterexample hunt for a formal result flagged as potentially flawed. Spawn this as a fresh subagent so the iterative Python script-writing, candidate-testing, and debugging output stays out of the main conversation. Returns a structured Markdown report. Use when the orchestrator (or user) needs to try to break a specific theorem/lemma — e.g. after `audit-proof` produces a `likely_flawed` verdict, or when the user explicitly asks to "find a counterexample to Lemma 4" / "try to break Theorem 3".

Cross-paper claim verification. When a paper restates a theorem or lemma from a cited prior work (e.g., "Theorem 1 (Liu-Layland)"), this agent fetches the cited source (with explicit user permission), locates the original statement, and compares against the restatement to detect subtle changes in preconditions, conclusion strength, or quantifier scope. Spawn as a fresh subagent so the web-fetch + reading workload stays out of the main context. Returns a structured comparison report.

Inject Proofreader audit findings as comment-only annotations into the paper's LaTeX source so the author can review them in their editor next to the actual proof text. Output is plain `%` comments that do NOT affect the rendered PDF and do NOT require any new packages. Produces a unified diff for review before applying. Triggers on "annotate my LaTeX with the findings", "add audit comments to my .tex", "patch my source with the audit results".

Deep audit of a single proof (theorem, lemma, corollary, or proposition). Use this when the user wants to scrutinize one specific formal result — checking logical gaps, assumption consistency, boundary cases, dependency correctness, and quantifier scope. Triggers on phrases like "audit the proof of Theorem N", "is this proof correct", "check the proof of Lemma M", "find issues in this proof".

First-pass author-facing review of a real-time systems (or related formal) paper. Use this when the user wants an overall quality assessment, score sheet, or an inventory of every formal result with per-result verdicts before submission. Triggers on phrases like "review my paper", "first pass on this draft", "score this submission", "list every theorem and flag the shaky ones".

Normalize a paper input (PDF, LaTeX source, multi-file LaTeX project, or pre-extracted text) into a clean structured representation that downstream Proofreader skills can consume. Use this once at the start of any non-trivial Proofreader session so the audit, counterexample, defender, and writeup skills don't each re-parse the source. Especially useful for LaTeX projects, where it preserves theorem-environment fidelity that PDF extraction loses. Triggers on "prepare this paper", "set up context for my .tex source", "extract theorems from this project", or when the user supplies a .tex / project root.

Draft a clean, self-contained technical brief documenting a correctness finding — usable to share with coauthors, to record in a project log, or to drop into a paper revision as the basis for a fix. Produces LaTeX or Markdown depending on the user's preference. Use when the user says "write this up", "draft a finding for X", "write a brief on the Theorem N issue", or after `audit-proof` + `find-counterexample` + `stress-test-defense` have produced material to synthesize.