Claude Code skill plugin for cleaning up, golfing, and bringing Lean 4 code up to mathlib standards
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…
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…
Command
Bump mathlib version and fix resulting breakage.
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.
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…
Command
Full file cleanup to mathlib standards (style audit + golf, methodical, no skipping).
Command
Contribute local learnings back to the mathlib-quality repo via PR.
Command
Break long proofs into helper lemmas.
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…
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.
Command
Fetch PR reviewer comments, implement fixes locally, gate the push behind explicit user approval, then watch CI to completion.
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.
Command
Process community learning contributions into reference docs.
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…
Command
Generate project declaration inventory for consolidation analysis.
Command
Pre-PR submission checklist.
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.…
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…
Command
Set up the ChatGPT MCP server for mathematical second opinions.
Command
Split large files (>1500 lines) into focused modules.
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.
Command
Teach the skill a new pattern or project convention.
Command
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 verso-blueprint as a…