Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add raja21068/AutoResearch --skill proof-checkergit clone --depth 1 https://github.com/raja21068/AutoResearchWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/raja21068/autoresearch/proof-checker)<a href="https://agentmods.dev/skills/raja21068/autoresearch/proof-checker"><img src="https://agentmods.dev/badge/skills/raja21068/autoresearch/proof-checker/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/raja21068/autoresearch/proof-checker"><img src="https://agentmods.dev/badge/skills/raja21068/autoresearch/proof-checker.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00090 | $0.10560 |
| Opus 5 | $0.00045 | $0.05280 |
| Sonnet 5 | $0.00018 | $0.02112 |
| Haiku 4.5 | $0.00009 | $0.01056 |
Grade A, and why
proof-checker scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 6d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 711 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Proof Checker: Rigorous Mathematical Verification & Fixing
Systematically verify a mathematical proof via cross-model adversarial review, fix identified gaps, re-review until convergence, and generate a detailed audit report with proof-obligation accounting.
Context: $ARGUMENTS
Constants
- MAX_REVIEW_ROUNDS = 3
- REVIEWER_MODEL =
gpt-5.4via Codex MCP, reasoning effort alwaysxhigh - REVIEWER_BACKEND =
codex— Default: Codex MCP (xhigh). Override with— reviewer: oracle-profor GPT-5.4 Pro via Oracle MCP. Seeshared-references/reviewer-routing.md. - AUDIT_DOC:
PROOF_AUDIT.mdat the paper directory root, alongsidemain.tex(cumulative log; when invoked via/paper-writing, this ispaper/PROOF_AUDIT.md) - REPORT_TEX:
proof_audit_report.tex(formal before/after PDF) - STATE_FILE:
PROOF_CHECK_STATE.json(for recovery) - SKELETON_DOC:
PROOF_SKELETON.md(micro-claim inventory)
Acceptance Gate (objective, replaces subjective scoring)
The proof passes when ALL of the following hold:
- Zero open FATAL or CRITICAL issues
- Every theorem/lemma has: (i) explicit hypotheses, (ii) proof with all interchanges justified, (iii) every application discharges hypotheses in the ledger
- All big-O/Θ/o statements have declared parameter dependence and uniformity scope
- Counterexample pass executed on all key lemmas (log candidates even if none found)
Issue Taxonomy (20 categories, 4 groups)
Group A: Logic & Proof Structure
| Category | Description | Example |
|---|---|---|
| UNJUSTIFIED_ASSERTION | Claim stated without proof or reference | "The Hessian splits into Gram blocks" |
| UNPROVEN_SUBCLAIM | "Clearly" / "it follows" hides a nontrivial lemma | "By symmetry, the cross-terms vanish" without checking |
| QUANTIFIER_ERROR | Wrong order ∀/∃, missing "for sufficiently small κ" | "For all π, there exists ε" vs "there exists ε for all π" |
| IMPLICATION_REVERSAL | Uses (A⇒B) as (B⇒A), or claims equivalence with only one direction | |
| CASE_INCOMPLETE | Misses boundary/degenerate cases | Singular covariance, zero weight, non-unique argmin |
| CIRCULAR_DEPENDENCY | Lemma uses theorem that depends on it | |
| LOGICAL_GAP | A step is not justified by what precedes it | B=Θ(1) → β_K=0 without analyzing W |
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 6d ago First seen · 711 lines · 90 tokens per session scan A 22b4d8210943
proof-checker is a skill published in the GitHub repository raja21068/AutoResearch (2 stars, last pushed 3mo ago), licensed MIT. It adds 90 tokens to every session and 10,560 once invoked, about $0.0005 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-03.
Other skills, from other repositories
content-refinement-agent
Step 5 of the PaperOrchestra pipeline (arXiv:2604.05018). Iteratively refine drafts/paper.tex by simulating peer review and applying targeted revisions, with strict accept/revert halt rules, deterministic 0-100 decision bands (Accept/Minor/Major/Reject) that drive a target-met early stop, and a Devil's Advocate…
section-writing-agent
Step 4 of the PaperOrchestra pipeline (arXiv:2604.05018). ONE single multimodal LLM call that drafts the remaining paper sections (Abstract, Methodology, Experiments, Conclusion), extracts numeric values from experimentallog.md into LaTeX booktabs tables, splices the generated figures from Step 2, and merges…
plotting-agent
Step 2 of the PaperOrchestra pipeline (arXiv:2604.05018). Execute the visualization plan from outline.json — render plots and conceptual diagrams from experimentallog.md and idea.md, optionally refine via VLM critique loop, and produce context-aware captions. Runs in parallel with the literature-review-agent. TRIGGER…
outline-agent
Step 1 of the PaperOrchestra pipeline (arXiv:2604.05018). Convert (idea.md, experimentallog.md, template.tex, conferenceguidelines.md) into a strict JSON outline containing a plotting plan, literature search plan (Intro + Related Work), and section-level writing plan with citation hints. TRIGGER when the orchestrator…
paper-autoraters
Run the four paper-quality autoraters from PaperOrchestra (arXiv:2604.05018, App. F.3) — Citation F1 (P0/P1 partition + Precision/Recall/F1), Literature Review Quality (6-axis 0-100 with anti-inflation rules), SxS Overall Paper Quality (side-by-side), and SxS Literature Review Quality (side-by-side). TRIGGER when the…
paper-writing-bench
Reverse-engineer raw materials (Sparse idea, Dense idea, experimental log) from an existing AI research paper to build a benchmark case for evaluating paper-writing pipelines. Replicates the PaperWritingBench dataset construction procedure from arXiv:2604.05018 §3 / App. C. TRIGGER when the user asks to "build a…