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 commands/cbirkbeck/mathlib-quality/expert-reviewgit clone --depth 1 https://github.com/CBirkbeck/mathlib-qualityWrote 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/commands/cbirkbeck/mathlib-quality/expert-review)<a href="https://agentmods.dev/commands/cbirkbeck/mathlib-quality/expert-review"><img src="https://agentmods.dev/badge/commands/cbirkbeck/mathlib-quality/expert-review.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.00038 | $0.09803 |
| Opus 5 | $0.00019 | $0.04901 |
| Sonnet 5 | $0.00008 | $0.01961 |
| Haiku 4.5 | $0.00004 | $0.00980 |
Grade A, and why
expert-review 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 4d 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 — 927 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/expert-review — Briefing for an External Mathematical Reviewer
Produce a single, self-contained mathematical document describing where the project is, what we're trying to do, what's done, what's stuck, and what we'd like the reviewer to weigh in on. Written for a mathematician who has no access to the repo, the Lean code, or the ticket board — only this document.
The output is REVIEW_BRIEF.md in the project root.
The hard rules:
- No Lean code unless a specific definition is mathematically essential and there's no
natural-language equivalent. Even then, render it like a mathematical statement, not
a piece of source code (no tactic blocks, no
:= by, no syntax peculiarities). - No file paths, no line numbers. The reviewer sees mathematics, not project metadata.
Refer to "the main theorem" and "Lemma 3.4" — never to
Mathlib/Foo/Bar.lean:123. - Self-contained: every notation introduced is defined; every cited result is stated (or has its statement faithfully summarised); every reference has a full citation.
- Detailed. A reviewer should be able to read this in isolation and give substantive guidance. Err on the side of more detail, not less.
What the brief may include (the user has explicitly allowed this):
- Ticket system details and ticket names. If the project uses a ticket board (e.g. via
/develop), describe its shape ("we have N tickets across these mathematical sub-goals") and use ticket names where they're mathematically meaningful (valenceFormula_main,q_expansion_principle). They're useful as a structural device for the "In progress" / "Targets" sections — the reviewer doesn't need to open a ticket, but referring to one by name lets the user follow the brief back to their work board afterwards. Drop opaque ticket IDs (numeric or hash-style); keep mathematical names.
Usage
The skill has two modes:
# Mode 1 — produce a brief and stop, waiting for the reviewer to reply
/expert-review # Brief covering the whole project
/expert-review <topic_or_subdir> # Brief restricted to one mathematical topic / subtree
/expert-review --update # Refresh the existing brief without re-asking context
# Mode 2 — integrate the reviewer's reply (run after they answer)
/expert-review --reply # Will prompt you to paste the reply
/expert-review --reply <path/to/reply.md> # Reply lives in a file
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.
- 4d ago First seen · 927 lines · 38 tokens per session scan A f252168dc1db
expert-review is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 15d ago), licensed MIT. It adds 38 tokens to every session and 9,803 once invoked, about $0.0002 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 commands, from other repositories
me-figure-discussion
Write or review thermal-fluid figure discussion with observation, physical mechanism, comparison, uncertainty, and claim limits.
master_analysis
Run comprehensive 5-phase analysis across labs, genetics, and protocols.
run-panguweather
Guide the user through running PanguWeather end-to-end on an AMD cluster.
render-figures
Compile all .tex and .typ figure files in a directory.
diff
Quantitative volume comparison between a CadQuery model and a reference STEP file.
arg-diagram
ARG academic-paper diagram mode — standalone structural & conceptual diagram generation.