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/buzzgit 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.00044 | $0.03926 |
| Opus 5 | $0.00022 | $0.01963 |
| Sonnet 5 | $0.00009 | $0.00785 |
| Haiku 4.5 | $0.00004 | $0.00393 |
Grade A, and why
buzz 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 — 280 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/buzz — Make Slow Proofs Fast
Find every declaration that elaborates slowly, work out why from the profiler and the traces, and fix it — target: each declaration under one second on the current machine.
The workflow this command automates is the one a mathlib reviewer applies to an AI-written PR: compile each file and watch the orange bars (the editor's still-elaborating indicator); for the few declarations whose bars linger, read the traces, find the issue, fix it — and then check the other slow declarations for the same issue before diagnosing them from scratch, because slow declarations written by the same author at the same time almost always share one root cause. That propagation step ("it's the same issue") is what makes the human version of this workflow fast, and it is binding here (Phase 5).
/buzz is a performance scalpel, not a general cleaner:
- Not golfing.
/cleanupmakes proofs short and idiomatic;/buzzmakes them fast. A proof can get longer here (a squeezed simp, an ascribedhave) if that's what speed costs. Run/cleanupafterwards if the edit got verbose. - Not decomposition. When the honest fix is splitting the proof,
/buzzflags/decompose-proofrather than doing the surgery itself. - The anti-
maxHeartbeatstool. Everywhere else in this plugin,set_option maxHeartbeatsis deleted on sight (/cleanup3.7,/pre-submit) with the instruction "optimize the proof instead" —/buzzis where that instruction gets carried out.
All measurement techniques, trace-reading instructions, and the root-cause taxonomy live
in references/profiling.md. Read it before Phase 3.
Usage
/buzz # PR mode: sweep the .lean files changed vs the default branch
# (merge-base diff + uncommitted changes)
/buzz <file.lean> # sweep one file
/buzz <file.lean> <decl> # one declaration, straight to Phase 3
/buzz --all # sweep every project .lean file (slow; use for audits)
/buzz --budget <ms> # per-declaration elaboration budget (default 1000)
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 · 280 lines · 44 tokens per session scan A df30d45c27c7
buzz is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 13d ago), licensed MIT. It adds 44 tokens to every session and 3,926 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
checklist
Generate a custom checklist for the current feature based on user requirements.
clarify
Identify underspecified areas in the current feature spec by asking up to 5 highly targeted clarification questions and encoding answers back into the spec.
specify
Create or update the feature specification from a natural language feature description.
analyze
Perform a non-destructive cross-artifact consistency and quality analysis across spec.md, plan.md, and tasks.md after task generation.
converge
Assess the current codebase against the feature's spec, plan, and tasks, then append any remaining unbuilt work as new tasks to tasks.md so implement can complete it.
implement
Execute the implementation plan by processing and executing all tasks defined in tasks.md.