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 skills/cbirkbeck/mathlib-quality/voyagernpx skills add CBirkbeck/mathlib-quality --skill voyagergit 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/skills/cbirkbeck/mathlib-quality/voyager)<a href="https://agentmods.dev/skills/cbirkbeck/mathlib-quality/voyager"><img src="https://agentmods.dev/badge/skills/cbirkbeck/mathlib-quality/voyager.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.00111 | $0.07943 |
| Opus 5 | $0.00056 | $0.03972 |
| Sonnet 5 | $0.00022 | $0.01589 |
| Haiku 4.5 | $0.00011 | $0.00794 |
Grade B, and why
voyager scanned grade B with 2 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 3d 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.
Asks for rootmediumPrivilege escalation
A mod that escalates privileges can change anything on the machine, not only the project.
`chmod 600`) and export them into the environment at the start of each run: Makes network callslowCapability
Not a fault in itself. Listed so you know the mod talks to something, and to what.
**Verify every link before posting**: curl the page (expect 200) and pull the real How it starts
The opening of the file, as written. The whole thing — 529 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Voyager — what's new in Tau Ceti
You are Voyager. Your job is to tell people about real mathematics that has newly landed in the Tau Ceti library, and to stay quiet otherwise.
The failure mode to avoid is not "missing something" — it is crying wolf. A message
listing foo_aux_2 and bar_eq_of_baz as exciting news trains everyone to ignore the
topic. One genuine named theorem is worth more than twenty declarations that merely have
names. "No notable named results this window" is a valid and frequent outcome — the
short check-in format in §6 exists precisely so you never have to dress up API glue as news.
Operators taking over the bot: read HANDOVER.md beside this file first — the state at
handover, the house style in worked detail, and the production lessons with their scars.
What counts
Post a result if it is a named mathematical result or a notable definition — something a mathematician would recognise as an object of study rather than a step in a proof. Concretely, in descending order of confidence:
- It has a Wikipedia page (Bochner's theorem, Riemann mapping theorem, de Finetti's theorem). This is decisive on its own.
- It is a named theorem/lemma/definition in a standard textbook or paper — cited as "Theorem 4.10 of Kedlaya", "Diamond–Shurman Thm 5.8.3", "Shimura §8.2".
- It is an eponym: Hungerbühler–Wasem, Atkin–Lehner–Li, Artin–Wedderburn, Gårding.
- It is a definition the rest of a subject is phrased in: the generalized winding number, the directing measure, Fredholm operators, Young symmetrizers.
Do not post:
- helper/auxiliary/private lemmas,
simplemmas,_eq/_apply/_def/_commAPI glue, instance boilerplate,omega-style arithmetic steps; - restatements, transports, or
variable-generalisations of something already announced; - anything already in Mathlib — see the novelty gate. The whole point of the topic is
what Tau Ceti adds, so an announcement of a theorem people can already
exact?from Mathlib is worse than useless; - a result whose proof still contains
sorryin its dependency cone.
What ships with it
2 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
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.
- 3d ago First seen · 529 lines · 111 tokens per session scan B 04f342beb861
voyager is a skill published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 15d ago), licensed MIT. It adds 111 tokens to every session and 7,943 once invoked, about $0.0006 per session on Opus 5. A static security scan graded it B with 2 findings (asks for root, makes network calls). No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
exploratory-data-analysis
Perform bounded, local exploratory analysis of explicitly supported scientific files. Use for redacted CSV/TSV/JSON profiles; optional NumPy, HDF5, FASTA/FASTQ, and basic image metadata inspection; missingness/leakage audits; outlier and transformation sensitivity; and rigorous EDA report scaffolds. Other domain…
nature-statistics
Audit, revise, or draft manuscript statistical reporting for Nature / high-impact journal submissions. Use when the user asks to check statistical analysis sections, p values, confidence intervals, sample size, biological versus technical replicates, randomization, blinding, multiple-comparison correction, model…
evaluating-with-leakage-gates
Evaluate an OpenMed de-identification or clinical NER model against the leakage-first release gates G1a through G8, which gate releases on residual PHI leakage rather than on F1. Use when the user wants to run the OpenMed eval harness on a synthetic golden set, decide whether a de-id model is RELEASABLE or…
mapping-to-snomed
Maps clinical concept spans extracted by OpenMed to SNOMED CT concepts through a USER-SUPPLIED terminology server (the user's own Ontoserver, Snowstorm, or UMLS/UTS), never a bundled vocabulary. Use when the user wants to code findings, disorders, procedures, body structures, or substances to SNOMED CT, run an ECL…
mixed-precision
Use FP16/BF16 mixed precision to accelerate training and reduce memory. Use when optimizing GPU performance.
indication-dossier
Build a source-backed biomedical indication dossier. Use when a research task asks for disease biology, target rationale, patient segmentation, biomarkers, trials, drugs, competitive landscape, or translational evidence.