mathlib-quality

Plugin mathlib-quality from marketplace mathlib-quality-plugins in CBirkbeck/mathlib-quality. Commands read from the repo's manifest — yesterday.

Skills (2)

• mathlib-quality

  Mathlib code quality and style enforcement for Lean 4

• voyager

  Post a "what's new in Tau Ceti" update as the voyager bot on the Lean Zulip — detect named theorems and significant definitions newly added to the TauCeti library since the last update, verify they are genuinely new (not already in Mathlib) and genuinely significant (via a ChatGPT second opinion), a

Slash commands (24)

• /mathlib-quality:beastmode

  Marathon work session. Pick up a ticket and stop at nothing to discharge it — fill every sorry, develop whatever API is needed, invoke /develop to plan more tickets whenever the path forks, and immediately work those tickets too. The session ends only when the target is fully proven or the work is g

• /mathlib-quality:blueprint

  Author or update the project's verso-blueprint — a Verso-based Lean module pairing each declaration with its mathematical statement and a paragraph-level proof sketch, producing an interactive HTML dep-graph + progress summary. Uses the standard `leanprover/verso-blueprint` tooling (the one behind v

• /mathlib-quality:bump-mathlib

  Bump mathlib version and fix resulting breakage

• /mathlib-quality:buzz

  Profile Lean declarations, find the slow ones, trace-diagnose the root cause, and fix them until each elaborates fast — ideally under a second. Statements never change; maxHeartbeats never goes up.

• /mathlib-quality:cleanup-all

  Project-wide cleanup using an orchestrator-worker pattern. The main session is the orchestrator — it does NOT read files, run lean_* tools, or edit. It dispatches batched per-file Agent calls with tight prompts (working dir + branch + build state + sequence + target), then narrates progress in one-l

• /mathlib-quality:cleanup

  Full file cleanup to mathlib standards (style audit + golf, methodical, no skipping)

• /mathlib-quality:contribute

  Contribute local learnings back to the mathlib-quality repo via PR

• /mathlib-quality:decompose-proof

  Break long proofs into helper lemmas

• /mathlib-quality:develop

  Plan a mathematical development project (planning-only). Searches mathlib, designs the API, then runs a binding **methodical decomposition pre-work pass** — for each top-level result, writes the prose proof, decomposes into ordered lemmas, **writes every lemma as a `:= by sorry` declaration in the p

• /mathlib-quality:expert-review

  Produce a self-contained mathematical briefing (no Lean, no file paths) for an external reviewer with no repo access — goals, plan, status, blockers, references, numbered questions

• /mathlib-quality:fix-pr-feedback

  Fetch PR reviewer comments, implement fixes locally, gate the push behind explicit user approval, then watch CI to completion

• /mathlib-quality:generalise

  Audit a lemma or definition for assumption-weakening opportunities — try mechanical weakenings, search the literature for the maximally-general form, auto-apply small safe changes, propose big changes for user approval

• /mathlib-quality:integrate-learnings

  Process community learning contributions into reference docs

• /mathlib-quality:mathlibable

  Decide whether a Lean declaration belongs in mathlib. Methodical, gated workflow that combines thorough literature search (WebSearch + ChatGPT MCP + local references + nLab/Stacks/MathOverflow for big decls) with mathlib's five-method exhaustive search, then a generality analysis against the literat

• /mathlib-quality:overview

  Generate project declaration inventory for consolidation analysis

• /mathlib-quality:pre-submit

  Pre-PR submission checklist

• /mathlib-quality:project-status

  Chat-only mathematical status of a /develop project. The agent reads the project's .lean files, identifies the result the worker is currently on (or blocked on), and reports in mathematical English what's being proved, where the proof sits, how it connects to the overall goal, and how far along the

• /mathlib-quality:redteam

  The Tau Ceti red team — an adversarial loop that audits the library file by file for wrong definitions, vacuous or mis-stated theorems, needless hypotheses, duplication of Mathlib or of other roadmaps, and code smells; confirms every big finding in Lean with a second opinion from gpt-6-astra; fixes

• /mathlib-quality:self-review

  Run N rounds of neutral, independent review-and-implement on your changes before a PR. Each round spawns a FRESH, unbiased review agent (techniques from the built-in /review and from /check-style, specialised to four Lean dimensions — definition necessity, generalisation, automation, mathlib naming/

• /mathlib-quality:setup-chatgpt

  Set up the ChatGPT MCP server for mathematical second opinions

• /mathlib-quality:split-file

  Split large files (>1500 lines) into focused modules

• /mathlib-quality:taupr

  The Tau Ceti worker loop — one unit of work per round, first that applies: rebase, fix CI, fix findings, review a stalled PR, else author a new one. Authoring checks the source material first, cleans up, and opens the PR; CI reviews it. We only self-review a PR that CI has left unreviewed for an hou

• /mathlib-quality:teach

  Teach the skill a new pattern or project convention

• /mathlib-quality:unformalise

  Turn a Lean declaration into mathematics. Renders the statement and a paragraph-level proof sketch as Unicode in the terminal by default (Γ, ℂ, →, ≤ — readable in chat without any math renderer). Optionally outputs Verso markup (`--verso`), Markdown (`--md`), or appends the result to the project's v

Hooks (2)

• Stop

  ${CLAUDE_PLUGIN_ROOT}/hooks/beastmode_stop.sh

• PreToolUse

  ${CLAUDE_PLUGIN_ROOT}/hooks/pr_gate.sh

Similar plugins