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/overviewgit 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.00009 | $0.07976 |
| Opus 5 | $0.00005 | $0.03988 |
| Sonnet 5 | $0.00002 | $0.01595 |
| Haiku 4.5 | $0.00001 | $0.00798 |
Grade A, and why
overview 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 — 712 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/overview - Deep Project Review
A slow, methodical review of the entire project. Produces a comprehensive inventory of every declaration, then performs deep analysis to find: moral duplications, generalization opportunities, missing API, and junk. This is not a quick scan. Take all the time needed. Do not skip steps.
Usage
/overview [directory_or_file] # full overview INCLUDING Step 9 mathlibable assessment
# (slow — full /mathlibable per public decl; plan on hours)
/overview [directory_or_file] --skip-mathlibable # everything except Step 9; faster draft view
Output: writes PROJECT_OVERVIEW.md in the project root. Per-decl mathlibable
detail reports go to .mathlib-quality/overview/mathlibable/<decl>.md.
Step 9 is the slowest by far. It dispatches one /mathlibable Agent per
non-skipped public declaration; each Agent runs the full 10-phase workflow
with the exhaustive nine-channel literature search. The orchestrator
narrates a one-line scoreboard between dispatches so you can leave the
session running. Use --skip-mathlibable when you want a fast structural
overview without the deep contribution assessment.
Philosophy
This command serves the same role as a senior mathematician reviewing a paper before submission:
- Are the definitions at the right level of generality?
- Are there lemmas that are morally the same and should be unified?
- Is there missing API that would make proofs cleaner?
- Are there definitions that shouldn't exist (duplicating mathlib or too specific)?
- Could results be stated more generally (rings instead of fields, etc.)?
Take your time. Read proofs carefully. Think about the mathematics, not just the syntax.
Phase 1: Inventory (Per-File Workers)
Step 1: Find Files
Find all .lean files (excluding .lake/, build/):
find . -name "*.lean" -not -path "./.lake/*" -not -path "./build/*" | sort
Step 2: Dispatch Per-File Inventory Agents
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 · 712 lines · 9 tokens per session scan A 55b31b886b40
overview is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 13d ago), licensed MIT. It adds 9 tokens to every session and 7,976 once invoked, about $0.0000 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.
constitution
Create or update the project constitution from interactive or provided principle inputs.
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.