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/generalisegit 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.00043 | $0.06339 |
| Opus 5 | $0.00022 | $0.03170 |
| Sonnet 5 | $0.00009 | $0.01268 |
| Haiku 4.5 | $0.00004 | $0.00634 |
Grade A, and why
generalise 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 — 604 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/generalise — Weaken Assumptions to Maximise Generality
Given a single lemma or definition, find every way its hypotheses can be weakened. Combines two passes:
- Mechanical pass — drop unused hypotheses, swap typeclasses for weaker ones from the
catalogue, point-localise global hypotheses. Each candidate is verified by
lean_diagnostic_messages. - Literature pass — online search (and ChatGPT, if MCP available) for the maximally general form known in the literature. Often the textbook statement is more general than what mathlib currently has.
Triage: small safe changes are auto-applied. Big changes (touch public API, restate the lemma, change typeclass to one with different operators) get presented to the user as a numbered menu of options with trade-offs — no auto-apply.
The hard rules:
- Verify after every weakening attempt. A weakening that breaks the proof is not a weakening; never leave the file in a broken state.
- Public API changes need user approval. A weakening that changes the call signature
of a public lemma (or
simplemma) is a big change, full stop. - Literature search is mandatory — the user explicitly asked for it. Skipping it is a defect.
- Every hypothesis must be examined — produce an artifact (the per-hypothesis status table) so a skipped hypothesis is detectable.
Usage
/generalise <file_path> <decl_name>
/generalise <file_path> # All public declarations in the file (one at a time)
A single declaration is the standard mode — generalisation is per-lemma surgery and shouldn't be batched casually.
Phases
PHASE 1 IDENTIFY find the declaration, its hypotheses, its proof
PHASE 2 CLASSIFY per-hypothesis: type-class? proposition? value?
PHASE 3 USAGE ANALYSIS find every use of every hypothesis in the proof body
PHASE 4 MECHANICAL drop-test + catalogue weakenings; verify each
PHASE 5 LITERATURE online search for max-generality form (REQUIRED)
PHASE 6 TRIAGE small safe vs big requires-approval; build the punch-list
PHASE 7 AUTO-APPLY apply the small changes; verify after each
PHASE 8 USER CHOICE present big-change options with trade-offs; STOP for approval
PHASE 9 APPLY + REPORT final apply + verification + report
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 · 604 lines · 43 tokens per session scan A 59a532b59328
generalise is a command published in the GitHub repository CBirkbeck/mathlib-quality (32 stars, last pushed 14d ago), licensed MIT. It adds 43 tokens to every session and 6,339 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
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.
paperfit-undo
作用: 恢复最近一次 PaperFit 自动写回前的备份版本，优先回滚主 .tex，必要时一并恢复 data/state.json。.
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.