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/developgit 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.00173 | $0.19305 |
| Opus 5 | $0.00086 | $0.09652 |
| Sonnet 5 | $0.00035 | $0.03861 |
| Haiku 4.5 | $0.00017 | $0.01930 |
Grade A, and why
develop 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 yesterday.
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 — 1,620 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/develop — Mathematical Development Planner
Plan a mathematical development. Creates a comprehensive plan from your references, designs the API for every new declaration, drafts the proof sketches step-by-step, and writes a detailed ticket board where every ticket contains the Lean statement and the full proof sketch with cited sources — detailed enough that no replanning is needed once execution starts.
/develop is planning-only. Workers don't run here. Once the ticket board is
approved, invoke /beastmode to pick up the next available ticket and work it to
completion.
This split keeps strategic thinking (mathlib search, API design, proof sketching from
sources, generality decisions) in /develop and tactical execution (state declaration,
call planned lemmas, iterate to compilation) in /beastmode. It prevents the
"agent reconsiders the whole approach mid-proof" failure mode — once /beastmode
starts a ticket, the plan is fixed; the worker either implements it or hard-stops with
a concrete reason it can't.
Source-faithfulness (BINDING — read before planning anything)
The single most expensive failure this command exists to prevent is a decomposition that drifts from the source's actual proof. When the plan's leaves are invented — chosen because they "look provable in Lean" or "connect to code we already have" rather than transcribed from the reference's own argument — the tree reliably bottoms out at a lemma the source never proves. That lemma is then either substantial mathlib-lacking infrastructure or outright false, and a worker burns a long session discovering it the hard way. Every recurrence has the same root cause: leaving the source.
The discipline that prevents it (enforced in Phase 1e and --decompose):
- Transcribe, don't invent. Read the reference's full proof (1e Step 1) and mirror its proposition chain. The source already did the decomposition; your leaves are its sub-results, named by their mathematical content — not a fresh route you happen to find convenient.
- Every leaf carries a precise source locator — statement number + page + a line/locator into
the reference text (e.g.
wedhorn.txt:2682). A leaf with no locator is suspect by default. - Acceptance test — quote-or-delete. For every leaf you must be able to quote, verbatim, the source passage that justifies it. If you cannot, it is an artifact: do not ticket it — go back to the source and find its real route.
- Two red flags that you have left the source — STOP and re-read the proof:
- the step needs you to build substantial infrastructure absent from mathlib, or
- a leaf turns out false (or only true under an extra hypothesis the source never uses). Both almost always mean the source proves the result a different, easier way.
- Never use memory or a prior summary as the source of a statement or a route. They drift
from both the reference and the code. Re-open the reference and the
.leanevery time.
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.
- yesterday First seen · 1,620 lines · 173 tokens per session scan A 0d45a4277f85
develop is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 13d ago), licensed MIT. It adds 173 tokens to every session and 19,305 once invoked, about $0.0009 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.