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/cleanup-allgit clone --depth 1 https://github.com/CBirkbeck/mathlib-qualityWhat 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.00120 | $0.04903 |
| Opus 5 | $0.00060 | $0.02452 |
| Sonnet 5 | $0.00024 | $0.00981 |
| Haiku 4.5 | $0.00012 | $0.00490 |
Grade A, and why
cleanup-all 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 2d 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 — 489 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/cleanup-all — Project-Wide Cleanup (Orchestrator Mode)
Run the full /cleanup workflow over every .lean file in the project, sustained
across hours or days, without exhausting the orchestrator's context.
The trick: the main session is an orchestrator, not an implementer. The
orchestrator dispatches batched Agent calls, each with a tight prompt and a
concrete target, then narrates progress in one-line scoreboards between
dispatches. The file reading, the LSP calls, the edits, and the per-declaration
golf all happen in subagent contexts — each starts fresh, does its batch,
returns a summary. The orchestrator never holds the work in its own context.
This pattern was observed in a real production session that ran for 28 days across 23 active days, dispatched 395 Agent calls, spawned 790 subagent contexts (workers spawning sub-workers), and survived 3 auto-compactions without losing the through-line. The mechanism is the orchestrator/worker split, not heroic context management.
Usage
/cleanup-all [directory]
If no argument, processes all .lean files under the project root (excluding
.lake/, build/, .git/).
The orchestrator's role (binding)
You are the orchestrator. Your job is to dispatch and track. You do NOT:
- Read project
.leanfiles — workers do that, they need the fresh context for it - Run
lean_diagnostic_messages,lean_goal,lean_multi_attempt, or anylean_*LSP query - Use
EditorWriteon project files - Run
lake buildyourself (workers do that as the first check of every batch) - Spot-check the worker's diff or rerun their LSP queries
You DO:
- Enumerate files (one
findcall, once) - Bucket files by size for batched dispatch
- Dispatch
Agentcalls following the verbatim prompt template below - Maintain a one-line scoreboard between dispatches
- Collect per-batch summaries from the workers' reports
- Dispatch one final verification Agent at the end
- Print the consolidated report at the very end
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.
- 2d ago First seen · 489 lines · 120 tokens per session scan A db7e5785d936
cleanup-all is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 14d ago), licensed MIT. It adds 120 tokens to every session and 4,903 once invoked, about $0.0006 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
cross-validate
Take a specific scientific claim and confirm or refute it across 3+ independent databases, then report concordance. Use before publishing, citing, or acting on a fact when you want to know how strongly it's supported. Forces multi-source verification that the agent doesn't naturally enforce.
translate-id
Resolve an identifier across all relevant namespaces (HGNC symbol, Ensembl, UniProt, NCBI Gene ID, RefSeq, MGI, OMIM, ChEMBL, PubChem, etc.). Detects the input namespace automatically, picks the right resolver tool, and returns a complete cross-reference table. Use when you have an ID in one namespace and need it in…
flow-nexus-neural
Train and deploy neural networks in distributed sandboxes.
check-dev
Type-check a Z specification with fuzz.
me-write-section
Draft or revise thermal-fluid manuscript, proposal, report, or thesis sections with clear paragraph logic, methods detail, assumptions, and figure-led discussion.
diff
Quantitative volume comparison between a CadQuery model and a reference STEP file.