CBirkbeck

CBirkbeck/mathlib-quality

Plugin Claude Code

Plugin marketplace listing 1 plugin: mathlib-quality.

CBirkbeck/mathlib-quality

Plugin Claude Code

Prove, clean up, golf, and bring Lean 4 code up to mathlib standards.

CBirkbeck/mathlib-quality

Instructions file

Instructions for CBirkbeck/mathlib-quality, covering claude context: mathlib-quality, project purpose, current status, completed and in progress / todo.

CBirkbeck/mathlib-quality

Command

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 genuinely outside…

CBirkbeck/mathlib-quality

Command

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 verso-sphere-packing…

CBirkbeck/mathlib-quality

Command

Bump mathlib version and fix resulting breakage.

CBirkbeck/mathlib-quality

Command

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.

CBirkbeck/mathlib-quality

Command

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-line scoreboards…

CBirkbeck/mathlib-quality

Command

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

CBirkbeck/mathlib-quality

Command

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

CBirkbeck/mathlib-quality

Command

Break long proofs into helper lemmas.

CBirkbeck/mathlib-quality

Command

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 project's Lean files (the…

CBirkbeck/mathlib-quality

Command

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.

CBirkbeck/mathlib-quality

Command

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

CBirkbeck/mathlib-quality

Command

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.

CBirkbeck/mathlib-quality

Command

Process community learning contributions into reference docs.

CBirkbeck/mathlib-quality

Command

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 literature-standard form…

CBirkbeck/mathlib-quality

Command

Generate project declaration inventory for consolidation analysis.

CBirkbeck/mathlib-quality

Command

Pre-PR submission checklist.

CBirkbeck/mathlib-quality

Command

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 whole project is.…

CBirkbeck/mathlib-quality

Command

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/style), reports its…

CBirkbeck/mathlib-quality

Command

Set up the ChatGPT MCP server for mathematical second opinions.

CBirkbeck/mathlib-quality

Command

Split large files (>1500 lines) into focused modules.

CBirkbeck/mathlib-quality

Command

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 hour.