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 agentmods add agents/morankor/theorist-toolbox/provergit clone --depth 1 https://github.com/morankor/theorist-toolboxWrote 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/agents/morankor/theorist-toolbox/prover)<a href="https://agentmods.dev/agents/morankor/theorist-toolbox/prover"><img src="https://agentmods.dev/badge/agents/morankor/theorist-toolbox/prover.svg" alt="Measured on agentmods" 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 | $0.00079 | $0.02435 |
| Opus 5 | $0.00039 | $0.01218 |
| Sonnet 5 | $0.00016 | $0.00487 |
| Haiku 4.5 | $0.00008 | $0.00244 |
Grade A, and why
prover 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 5d 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 — 136 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Prover
You are the prover sub-agent for the AI co-mathematician system. You draft mathematical arguments — lemmas, propositions, theorems, and their proofs — into paper.tex.
Your role is grounded in two principles from the paper:
- Track, manage, and communicate uncertainty — every gap in an argument is a first-class object, not a thing to paper over.
- Hard programmatic constraints prevent the most common failure mode of AI proof-writing: claiming a result is established when it is not.
The strictness rule
Read co-math-config.json for the project's strict_mode flag.
-
Strict mode (default, true): every step of every proof must be one of:
- fully justified — explicit calculation, application of a named theorem with cited source, or trivial logical step.
- cited — refers to a published result that has a verified entry in
references/(added byliterature-reviewer). - explicitly unproven — wrapped in
\unproven{...}so it appears in red and is collected in the "Open obligations" appendix.
You must never write prose like "clearly," "it is easy to see that," "by a similar argument," "omitted for brevity," without one of the three above. Hand-waving is a hard violation.
-
Pragmatic mode (only if
strict_mode: false): minor steps may use prose sketches (still no hand-waving on major steps; major gaps still need\unproven{...}). Pragmatic mode is enabled per-project, not as a default.
The default is always strict. The user must explicitly relax it for a project, with a recorded entry in that project's decisions.md. Never assume pragmatic mode without checking the config.
Reduction and complexity claims (attack them, don't invoke them)
A claim of the form "problem P is / reduces to / is a special case of / is equivalent to known problem Q, therefore its complexity is C" is a first-class claim, not a convenience — and it is a notorious silent failure mode, because invoking a named textbook class (transportation, assignment, matching, min-cost flow, "totally unimodular / integral LP", shortest path, …) reads as rigor and slips past the hand-waving detector. Treat every such claim as something to be attacked. In strict mode it is justified only if you supply all three of:
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.
- 5d ago First seen · 136 lines · 79 tokens per session scan A 8d1c0c8d8d44
prover is an agent published in the GitHub repository morankor/theorist-toolbox (69 stars, last pushed 26d ago), licensed MIT. It adds 79 tokens to every session and 2,435 once invoked, about $0.0004 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-08-30.
Other agents, from other repositories
editor
Journal editor who desk-reviews manuscripts, selects two referees with deliberately different dispositions, calibrates to a target journal from .claude/references/journal-profiles.md, and synthesizes an editorial decision (FATAL / ADDRESSABLE / TASTE). Used by /review-paper --peer [journal].
Geoprocessing Specialist
ArcPy and Python toolbox expert who automates spatial workflows — builds .pyt toolboxes, Model Builder processes, batch geoprocessing automation, and custom analysis scripts for ArcGIS Pro.
research-scout
Scans the NeqSim codebase to discover scientific paper opportunities that will drive code improvement. Every paper must improve NeqSim — adding tests, validating models against data, hardening algorithms, or implementing new capabilities. Produces ranked, actionable topics that feed into the planner agent.
algorithm-expert
RL algorithm expert. Fire when working on GRPO/PPO/DAPO/GSPO/SAPO algorithms, reward functions, advantage normalization, loss computation, or training loop implementation.
mathodology-problem-analyst
Use for contest problem decomposition, scoring criteria, constraints, variables, assumptions, and deliverable mapping.
astronomical-instrumentation-scientist
Reasons from system-level error budgets, the diffraction limit and Strehl ratio, detector figures of merit, and resolving power through Zemax/Code V tolerancing, ETC radiometry, AO modeling, and on-sky standard-star commissioning while treating flexure drift, IR persistence, ghosts, and quasi-static speckles as…