mathlib-quality CLAUDE.md

Claude Context: mathlib-quality

Project Purpose

A Claude Code skill plugin for cleaning up, golfing, and bringing Lean 4 code up to mathlib standards before PR submission.

Current Status

Version: 0.73.1

Completed

• Plugin architecture with 23 commands defined in commands/
• Reference documentation in skills/mathlib-quality/references/
• Data collection scripts in scripts/
• Lean 4 integration docs in .claude/docs/lean4/

In Progress / TODO

1. Testing the Plugin - Need to verify commands work in Claude Code with actual Lean files

Community Learnings

• Contributions arrive as JSONL files in data/community_learnings/ via /contribute PRs.
• /integrate-learnings propagates them into the reference docs only — no RAG, no MCP server.
• Historical reference docs (references/style-rules.md, references/naming-conventions.md, references/proof-patterns.md, references/pr-feedback-examples.md) were originally seeded from a scraped corpus of mathlib4 PR reviews. The scraped data was removed in v0.46.0 — the curated reference docs themselves remain the source of truth.

Key Files

File	Purpose
.claude-plugin/plugin.json	Plugin manifest and command definitions
skills/mathlib-quality/SKILL.md	Main skill activation triggers
commands/*.md	Individual command implementations
skills/mathlib-quality/references/*.md	Style rules, naming, patterns
scripts/style_checker.sh	Local Lean file style validation

Commands Available

• /develop - Planning-only with binding methodical-decomposition pre-work. Phases 1a–1d gather context, study references, search mathlib, design the API. Phase 1e (binding): (Step 1) read the source's FULL proof of each result, including every sub-lemma the source itself uses — page-by-page, not headline+summary. (Step 2) decompose by mirroring the source's own sub-lemma structure — every named sub-lemma the source proves is a candidate leaf; recurse only when the source's proof of a sub-lemma is itself multi-step; multi-part statements split one leaf per part (top-level ∧-chains, source parts (i)/(ii)/(iii) — any kept bundle is a one-line ⟨…⟩ assembly node; shared-witness existentials and simultaneous-induction bundles are the documented exceptions, per references/statement-splitting.md). LOC estimates must cite the source line count of the corresponding sub-proof; ungrounded estimates are forbidden. (Step 2.5) physically state every lemma in Lean as := by sorry — skeleton must lake build clean. (Step 3) verbatim source quote per leaf + Lean ↔ source match. (Step 4) per-leaf provability check (mathlib / project / API gap). (Step 4.5) disproof attempt — negation search, edge-case instantiation, hypothesis-strength test, implausibility check. (Step 4.6) consult .mathlib-quality/b2_log.jsonl (which /beastmode writes on B2 stops) for prior-B2 name/shape matches. (Step 5) seven-condition confidence gate including source-mirror structure and statement-shape (one-conclusion-per-leaf) checks. (Step 6) write decomposition.md. Source-gap fallback chain: if a sub-result is opaque in the cited source, cross-reference other references, then search the wider literature, and as a last resort file a numbered question in /expert-review — affected leaves enter REVIEW-PENDING status; the confidence gate does not pass for them; tickets are not created until the reviewer's answer is integrated via /expert-review --reply. Tickets (1g) only after every gate passes. Flag --decompose runs ONLY Phase 1e and stops, in ADVERSARIAL mode: worker's primary disposition is opposing the plan, not building it. Every leaf must survive ≥3 distinct attacks across five categories (counterexample search, edge-case instantiation, hypothesis-strength test, source-drift attack, discharge attack); every internal node attacked on composition. Empty/shallow attack logs block the gate.
• /beastmode - Marathon work session. Stops at nothing — but stays on-target. Picks a ticket and finishes the goal no matter how deep the path goes. Spawns sub-tickets in /develop's template format for missing lemmas/dependencies; invokes /develop --continue to replan when a sketch is wrong as a strategy; no recursion cap, no time budget. Statement-splitting (Tier A5): a ticket or would-be sub-ticket bundling several independently-provable conclusions (top-level ∧-chain, source parts (i)/(ii)/(iii)) is split — one sub-ticket per part, the bundled declaration discharged as a one-line ⟨…⟩ assembly (references/statement-splitting.md). Continuously checks on-target: before each sub-ticket and each new step, confirms (1) it serves the main goal in plan.md, (2) it stays in the project's mathematical area, (3) it's a refinement not a divergence. Welcomes scope growth that stays on target — a step estimated as two lemmas turning out to be ten is great news (= more mathematics captured), not a stop signal. The harder the work, the more energy goes in — Super Saiyan ethos. Mandatory Phase 6.5 post-proof cleanup: after gates pass and before mark-done, beastmode invokes Skill(skill="mathlib-quality:cleanup", args="<file> <decl_name>") on every new declaration the ticket produced — full 11-phase /cleanup workflow, no phase-skipping (enforced via /cleanup's own phase checklist), simplify (6.5) and buzz (6.6 performance) hand-offs mandatory, so freshly-proven declarations come out fast as well as clean. Decompose flags spawn /decompose-proof sub-tickets; rename queue is drained inside /cleanup's Phase 5b; gate failures from /cleanup block ticket completion. Only legitimate stops: DONE / SCOPE-DEFINITION ERROR (statement actually wrong) / OFF-TRACK (drift onto material outside the project's mathematical scope, with concrete evidence — plan-paragraph contradiction or published-theorem-scale gap) / BROKEN BASELINE (lake build broken on entry). "It's hard", "it's late", "we're N sub-tickets deep", "this is taking a while", "this is multi-session work" — none of these stop beastmode. Multi-session work is the target signal, not the exit: beastmode exists to collapse what would otherwise be multi-session work into one continuous run.
• /cleanup - 11-phase methodical workflow: doctor (baseline build, abort if broken) → prepare (incl. module-system dialect probe) → style-audit punch-list → file-level fixes (section headers PRESERVED; imports skipped on module files) → per-declaration deep golf (with diff gates AND a Step-6 phase-checklist artifact so skipped phases are detectable; proof comments are PRESERVED and re-anchored — the strip-comments rule was reversed in v0.58.0 per live maintainer feedback) → Phase 5a non-rename refactoring + Phase 5b dedicated rename pass (Phase-4 workers never rename in place; they append to .mathlib-quality/renames.jsonl and Phase 5b consumes the queue with one sequential repo-wide pass — eliminates parallel-worker rename races) → final-gates + cumulative checks (build gates are cited tool-call gates — the actual lake build invocation + exit status per touched module, hard stop on failure; plus comment-preservation and new-identifier hallucination checks; LSP-unavailable workers are re-dispatched, never counted done) → Phase 6.5 hand-off to the built-in /simplify skill for holistic review → Phase 6.6 hand-off to /buzz (performance pass: every decl under the elaboration budget; deferrals feed /decompose-proof; big perf changes flagged for approval) → report. Absorbed /check-style (Phase 2 audit), /check-mathlib (Phase 4 item 13: five-method search + six strict rules + common-equivalents lookup — references/mathlib-search.md), the inline mechanical pass of /generalise (Phase 4 item 18), and shouyi-style diff gates (references/cleanup-gates.md).
• /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 enumerates files, buckets by size (Tiny 6-10 per batch, Small 3-5, Medium 1-2, Large 1), dispatches batched Agent calls with a tight ~1200-char verbatim prompt (working dir + branch + build state + sequential file list + target), and narrates progress in one-line scoreboards between dispatches (**T lines remaining. K/N files done (P%).** Continuing.). The actual cleanup happens in fresh subagent contexts — workers read files, run LSP, dispatch per-declaration Phase-4 sub-workers, run the build, return compact summaries with a required Phase checklist (P1–P7, including 5a, 6.5 and 6.6) so any skipped phase triggers a single-file re-dispatch. Workers never apply cross-file renames inline; they append to the project-wide queue at .mathlib-quality/renames.jsonl. After all per-file batches return, the orchestrator's Step 5 drains the queue in a single repo-wide Phase 5b dispatch. Forbidden orchestrator patterns: "Let me verify ...", "Let me run lake build", "Quick sanity check", "Continuing now". The pattern that sustained a real 28-day, 9000-message, 395-dispatch, 790-subagent marathon without context exhaustion.
• /decompose-proof - Break long proofs into helpers (two-pass: analysis with DECOMPOSE plans → parallel agent decomposition)
• /buzz - Profile → trace → fix slow declarations; target <1s each. The reviewer workflow ("compile each file, watch the orange bars; for lingering decls read the traces, find the issue, fix it — then check the other slow decls for the same issue") as a command. Sweep: one profiled compile per target file (lake env lean -Dprofiler=true -Dprofiler.threshold=100), per-decl timing table; SLOW = over --budget (default 1000ms); decls carrying a maxHeartbeats raise are SLOW by definition. Diagnose worst-first via escalation ladder — lean_profile_proof → trace.profiler tree → targeted traces (synthInstance / isDefEq / simp.rewrite / diagnostics) — classified against the eight-cause taxonomy in references/profiling.md (instance-synthesis blowup, fat simp, defeq blowup, heavy terminal automation, mvar churn, coercion churn, duplicated subterms, kernel replay). Phase 5 same-issue propagation (binding): test root cause #1 on every remaining slow decl before any fresh diagnosis — one PR's slow decls nearly always share a cause. Binding rules: statements byte-identical (theorem_statement_protected); limits never raised (existing raises removed per decl); no native_decide/sorry; all profiling scaffolding reverted (gate greps for it); global fixes (shortcut instances, priorities, file-wide attributes) flagged for user approval, never auto-applied. Deferral requires ≥3 measured fix attempts and routes to /decompose-proof. Modes: bare = changed files vs default branch (PR mode), <file>, <file> <decl>, --all, --budget <ms>. Report: before/after table (ms + heartbeats), root causes, removed raises, deferrals, flagged-changes menu. Also runs automatically as /cleanup's Phase 6.6 (and hence inside /beastmode's post-proof cleanup and /cleanup-all workers).
• /overview - Project survey + per-decl mathlibable assessment. Per-file inventory (kind/name/description/deps) + deep cross-file analysis (mathlib API audit, moral duplications, generalisation opportunities, missing API, junk identification) + Step 9 Mathlibable Assessment: pre-filters obvious SKIPs (private, _aux, name-collides-with-mathlib, etc.), then dispatches one Skill(mathlib-quality:mathlibable) Agent per remaining public decl running the full 10-phase workflow per decl (exhaustive nine-channel literature search + generality + modern-idiom check + diamond/defeq risk + mathlib five-method search + composition check + five-bucket verdict). Sequential dispatch with one-line scoreboard between (**K/N decls assessed. R YES-add-as-is, S YES-but-generalise, …** Continuing.); each Agent's full Phase-8 report stored at .mathlib-quality/overview/mathlibable/<decl>.md. Writes PROJECT_OVERVIEW.md aggregating verdicts into per-bucket action lists (open mathlib PR / run /generalise / delete + reuse / inline composition / open questions). Step 9 is hours-long on 50-decl projects; pass --skip-mathlibable for a faster draft view that runs all other steps.
• /project-status - Chat-only mathematical status of a /develop project. The agent reads the project's .lean files (plus .mathlib-quality/plan.md and tickets.md if present) and reports in mathematical English: what result the worker is currently on, what (if anything) is blocked and what is mathematically missing, how the current work connects to the project's overall goal, and how far along the whole project is. Read-only — no server, no browser, no sidecar files. Audience is an expert mathematician glancing between work sessions; tone is descriptive math reportage, not difficulty rhetoric.
• /expert-review - Two-mode external-review workflow. Mode 1 produces a self-contained REVIEW_BRIEF.md (no Lean, no file paths) with goals, plan, references, established results, in-progress work, blockers, numbered questions, then stops and waits. Mode 2 (/expert-review --reply) takes the reviewer's response, maps it onto the questions, and proposes ticket/work-order updates — applies only after user approval. State persists in .mathlib-quality/expert-review/<date>/. Ticket names allowed where mathematically meaningful.
• /generalise - Weaken a lemma's or def's assumptions. Tries mechanical weakenings from references/generalisation-patterns.md (typeclass parents, drop-unused, point-localise, strict→weak); does a mandatory literature search (WebSearch + ChatGPT MCP + mathlib search). Small safe changes auto-apply with verification; big changes (public-API, renames, restating) become a numbered options menu for user approval — no auto-apply.
• /taupr - The Tau Ceti worker loop, modelled on the reference worker (kim-em/TauCetiWorker): a round does exactly one unit of work — the first that applies. R1 REBASE (genuine TauCeti/ conflict after a sibling merged) → R2 FIX-CI (build red — outranks R3, since a PR that does not build cannot be reviewed) → R3 FIX (findings: fix the code, or contest in the rubric thread the finding came from) → R4 REVIEW (fallback only: green build, no scoreboard at the current head, and ≥1h since the build status — CI reviews automatically once the build is green, so posting sooner spends your subscription on work the project was about to do free) → R5 AUTHOR (open a new PR) — capped at 3 of our own PRs open (--max-open, 0 lifts it), else the round reports IDLE. The cap is load-bearing: a PR that is still building is not red, has no findings and is not yet reviewable, so no step catches it and the board reads as quiet — and R4's one-hour wait makes a green PR look like nothing to do for that whole hour. Uncapped, a ten-minute loop authors a new PR every tick. IDLE is a correct outcome: it means the work in flight is waiting on someone else. Maintenance outranks authoring so in-flight PRs are not starved; merging, closing and dedup are the repo's CI, not this loop; and a GitHub API failure aborts the round rather than reading as "nothing to do" and falling through to authoring duplicate PRs. R5: intake once per chain → check the source material first (roadmap as written → review-quality library code → adapting the named source; pinned clone, index-before-grep, three vocabularies, read the neighbourhood, sub-lemma check) so we do not rebuild mathematics that exists → /develop+/beastmode → /cleanup on every changed file + /decompose-proof (>30 lines; 50 cap) → PR body (Roadmap: line on every PR per AGENTS.md; the tauceti-target marker only when authoring a roadmap target per COORDINATION.md §4 [COOP] — a refactor carries the Roadmap line but NO marker, since it advances no target and so has no deterministic id; inventing one is the free-form slug the contract forbids and a colliding fabricated id would let the sweeper close a legitimate PR. For a refactor, invisibility to dedup is correct — two refactors of one file are a merge conflict, not a target duplicate; provenance) → --force-with-lease push + create → round ends; CI reviews it. The pre-PR gate (hooks/pr_gate.sh) blocks gh pr create on the cheap checks only — cleanup[] covering every changed .lean file (list computed from git diff merge-base..HEAD, so under-reporting fails and names the misses), source_sweep[] with pinned revisions + literal queries, and a fresh duplication_check. Review fields are optional, since there is no pre-PR review to wait on; a recorded red review still blocks. Reviews are pinned to codex (--reviewer codex): independence from the model that wrote the Lean, and on macOS only codex gets a real clean room (~/.codex/auth.json is a file copied into a throwaway CODEX_HOME; ~/.claude/.credentials.json is absent under a Keychain login, so the Claude reviewer falls back to the real HOME). Runs ONE round per invocation — it has no loop flag of its own; recurrence comes from the harness (/loop 10m /taupr in-session, or a cron via the schedule skill), as /beastmode does. The interval is only the polling cadence: it sets how fast a red build or fresh finding is noticed and does not move R4's one-hour threshold, which is measured from the build status timestamp. Also --only/--skip over the cascade, status, --review-age. Mechanics in references/tauceti.md.
• /pre-submit - Pre-PR submission checklist — 10 gated steps, each with a required artifact. Step 0a chain intake — asks ONCE per PR chain (not per PR) what the chain delivers, which roadmap area/target family it lands in, and from what source (upstream repo / sibling project / paper + revision + license, or "original work"), then persists the answers to .mathlib-quality/pr-session.json; every later PR reads that file instead of re-prompting, and each branch's specific one-line description + target marker are DERIVED from the diff, never asked. --reset-intake re-asks when the chain's provenance actually changes → Step 0b sources before code — the source sweep is a cited gate, not a tick-box: per roadmap-named upstream repo, a pinned clone (repo@sha — a worker who never cloned can't produce one, which is what makes it checkable), index-before-grep (blueprint / dep graph / ## Main results / README), three vocabularies (yours, the source's convention, and the operator that cannot be renamed away — the one that actually finds things), read the neighbourhood not the grep hits (results live as unnamed haves inside larger proofs), and a sub-lemma check (if the source proves something needing your result, read that proof) → port and adapt, never rederive. Plus pinned mathlib + the repo's own OPEN PRs, all checked before any new Lean was written — a result can be absent from main, absent from mathlib, and still already written in an open PR, most often your own earlier branch in the same chain, since Step 9 deliberately keeps several in flight; overlap ranked by same-target-marker → same-decl-names → same-files → same-source-section, and an unresolved overlap is a hard stop; a declaration claiming mathlib-absence on a search-only basis is a hard stop — absence needs an untruncated full-name grep and a compiled example probe, because typeclass-derived and auto-generated results are text nowhere) → build → /cleanup → linters → debug-artifact scan → axiom check (catches hidden sorryAx) → docstrings → final build → Step 8 local review-rubric dry run: on repos gated behind a scriptable reviewer, run the review engine on the LOCAL branch (--diff-file / --pr-desc-file / --no-post — no PR need exist; stage git archive of the branch head, a fresh roadmap clone, a symlink to the pinned mathlib, and a merge-base diff) and iterate until every rubric is green, re-checking the open PRs here too (Step 0b's check is hours stale by now — this is the one that catches the race), writing .mathlib-quality/review-receipt.json (head_sha + all_green + per-rubric verdicts + literal invocation + exit code + a duplication_check recording PRs examined and overlaps) — and the plugin's PreToolUse hook hooks/pr_gate.sh mechanically BLOCKS gh pr create until that receipt exists, is green, and matches the current HEAD, because instruction text did not hold: opening a PR and waiting for the server reviewer is easier and feels like progress, so the fix is making the shortcut the blocked path. Stale receipts (branch moved since review) block too, as does a missing/stale duplication_check, an unacknowledged overlap, a source_sweep entry lacking a full revision or literal queries, or an empty source_sweep when the Step-0a intake named a source (cross-checked against pr-session.json, closing the cheapest bypass) — a deliberate stacked follow-up is recorded acknowledged: true with a note, not deleted. Gate is armed by the Step-0a session file (inert everywhere else), fails open on infrastructure trouble, and escapes via PR_GATE_OVERRIDE=1 or .mathlib-quality/pr_gate_disabled → Step 9 pipeline (advisory: 10-min cron on open PRs reading scoreboard head_sha not labels, next candidates taken through Steps 0–8 meanwhile). Full workflow in references/pr-workflow.md.
• /self-review - N rounds of neutral, independent review-and-implement before a PR (default 3; /self-review n sets n). Each round is one review + one implementation; the loop runs exactly n rounds and stops after the nth implementation, even if the code is not perfect. Review: dispatch a fresh, independent review Agent (a new Agent per round — never SendMessage, so no round anchors on the last and no reviewer has an ego stake in its earlier comments). The reviewer applies techniques from the built-in /review + /code-review (verify-before-report, steelman the author's choice before a finding stands) and /check-style (now /cleanup Phase 2 + the style/naming references), specialised to four Lean dimensions: (1) definition necessity — is much lost if a def were notation/abbrev/inlined? (a def earns its keep by carrying valuable data, encoding a propositional quality, or hiding a horrendous construction proofs never unfold; a def whose internals get unfolded everywhere is a flag); (2) generalisation — to what extent and in what way (typeclass parents, drop-unused, point-localise, strict→weak, concrete→abstract; references/generalisation-patterns.md), tested where cheap; (3) automation — best use of simp/grind/aesop/fun_prop/omega/project-local tactics, with the binding principle that deterministic automation beats a long non-deterministic hand-rolled (LLM-style) proof, claims tested via lean_multi_attempt; (4) mathlib naming/style (defs lowerCamelCase, lemmas snake_case, types UpperCamelCase, C_of_A_of_B, ≤/< orientation, comment-preserving golf — signposts stay, deleted ones get flagged — etc.; not the things linters already catch). The reviewer stays objective, open-minded, and self-sceptical but not paralysed, and the round number never softens its standard — it never rubber-stamps, not even on the final round; termination is the loop's fixed n, not the reviewer's call. The driving instance then (i) reports the requested changes to the user and posts them to the PR thread if one exists (else chat-only; --no-pr forces chat-only), (ii) implements every suggestion — the only permitted non-implementation is a change that breaks the build or is incorrect, which is attempted → reverted → documented for the next round (never silently skipped; disagreement is not grounds to skip), (iii) reports a summary of what changed, (iv) relaunches a fresh reviewer for the next round unless n rounds are done. No commits, no pushes — changes are left in the working tree. Scope: bare = changed .lean files vs the base branch (PR mode); also <file>, <file> <decl>.
• /fix-pr-feedback - Address reviewer comments. Fetches all comments, implements fixes locally, stops for explicit user approval before pushing, then watches CI to completion (using gh pr checks --watch in background as the wake mechanism). Tau Ceti mode (repo-specific, verified against the TauCeti/TauCetiReview repos — references/tauceti.md): the review agents are the feedback, not bots to filter (never drop tauceti-scoreboard / tauceti-rubric: comments); state comes from the newest scoreboard comment's <!--tauceti-meta:v1 …--> JSON (head_sha + per-rubric states), never the label, never scraped Markdown, and a review binds only to the head_sha it names; a contest is a REPLY IN THE RUBRIC THREAD THE FINDING CAME FROM (POST /repos/…/pulls/<PR>/comments/<ROOT_ID>/replies) — a top-level gh pr comment is a different endpoint and is silently ignored, as is any comment whose body contains tauceti-reply:/tauceti-rubric: (so quote the conflicting thread's prose and strip the markers); contest only a genuine contradiction and show it (link + quote rubric/round); a contest does not re-trigger CI — the local worker owns it, so run tauceti-review <PR> afterwards, and /review on its own line re-triggers a full CI review; pushes are --force-with-lease against the observed head ([HARD] coordination rule, never a plain push); never --admin-merge and never strip a PR's human-owned scripts//.github//lakefile changes to chase auto-merge.
• /bump-mathlib - Bump mathlib version and fix resulting breakage
• /mathlibable - Decide whether a Lean declaration belongs in mathlib. Slow, methodical, gated workflow — the slowness is the point. Ten phases: doctor → comprehend (write the math statement in prose) → preliminary checks (BIG/SMALL is recorded for narrative only; the literature width is always EXHAUSTIVE; one-line check with defeq-abuse / typeclass-diamond / API-stability exemptions) → EXHAUSTIVE literature search (mandatory, every invocation): WebSearch ×≥3 at varying generality + ChatGPT MCP (asks about historical formulation evolution) + local refs + nLab + nCatLab + Stacks + MathOverflow + arXiv. There is no --quick / --exhaustive flag — every call does the full sweep. → generality analysis: (4b) current vs literature-standard, (4c) modern-mathlib-idiom restatement — the Bourbaki 2.0 check asking whether mathlib's contemporary tools (typeclasses over preambles, filters over sequences, universal properties over constructions, bundled types over set-with-closure, modules over vector spaces, higher categories over 1-categories) would re-state the result with real downstream consequences → diamond/defeq risk for def/class/instance → mathlib five-method search on BOTH the user's form AND the literature-standard form AND the modern-idiom form → composition check (≤3 mathlib calls?) → verdict: YES-add-as-is | YES-but-generalise-first | NO-mathlib-has-it | NO-composable-from-mathlib | BORDERLINE-needs-human. Cost is NOT a verdict factor — mathlib is Bourbaki 2.0, EXPENSIVE generalisations are explicitly worth doing. Each verdict bucket requires documented evidence; Phase 7 gate rejects unsupported verdicts and rejects "too expensive to generalise" rationales (those are BORDERLINE questions, not self-resolving downgrades). Single declaration per invocation. Worked examples per bucket + the Bourbaki 2.0 philosophy + canonical modernisation cases (modules-not-vector-spaces, filters-not-sequences, Submodule not closed-subset-predicate, mathlib's measure-theory triple, universal-property limits) in references/mathlibable-verdicts.md.
• /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 leanprover/verso-blueprint (the tool behind verso-sphere-packing, verso-flt, verso-carleson, verso-noperthedron); chapter files are .lean modules under <Project>/Chapters/, statements are :::theorem "label" (lean := "Foo.bar") directives, dep-graph edges are {uses "label"}[], math is KaTeX. Verso auto-computes completion status from the (lean := …) reference — no manual \leanok to keep in sync. Seven phases: doctor (verso scaffold + lake build + lake env probe) → enumerate (diff existing chapters to compute New/Drift/Stale sets) → plan (user confirms scope) → prose context → author (one worker per declaration; Verso directives only) → cross-link pass (orphan {uses} resolved; stale (lean := …) repaired; Blueprint.lean import/include sync) → hand-off (./scripts/ci-pages.sh, verify _out/site/html-multi/). Modes: whole project (default), single file, --decl <Foo.bar> (single decl + closure), --update (drift-only), --check (inventory + diff, no authoring), --migrate-from-latex [<dir>] (one-shot mechanical 1:1 conversion of a legacy leanblueprint LaTeX tree). Conventions + Verso-specific deployment gotchas in references/blueprint-conventions.md.
• /unformalise - Turn one 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), then asks whether to (b) append to the verso-blueprint, (v) print as Verso markup, (m) print as Markdown, or (n) terminal-only. Non-interactive flags --verso / --md / --blueprint skip the prompt. Single-declaration default; --closure walks the dependency closure; whole .lean file also allowed. Shares the unformalisation worker logic and conventions with /blueprint Phase 4 (same references/blueprint-conventions.md). Use when you want to see the math first; /blueprint --decl is the non-interactive variant.
• /setup-chatgpt - Set up ChatGPT MCP server for mathematical second opinions (requires ChatGPT desktop app + Plus/Pro)