# Mathlib Quality

> Mathlib code quality and style enforcement for Lean 4

- **Type:** Skill
- **Install:** `agentstack add skill-cbirkbeck-mathlib-quality-mathlib-quality`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [CBirkbeck](https://agentstack.voostack.com/s/cbirkbeck)
- **Installs:** 0
- **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills)
- **Latest version:** 0.1.0
- **License:** MIT
- **Upstream author:** [CBirkbeck](https://github.com/CBirkbeck)
- **Source:** https://github.com/CBirkbeck/mathlib-quality/tree/main/skills/mathlib-quality

## Install

```sh
agentstack add skill-cbirkbeck-mathlib-quality-mathlib-quality
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# Mathlib Quality Skill

## Activation Triggers

This skill activates when:
- Working with `.lean` files intended for mathlib contribution
- User mentions "mathlib style", "cleanup", "golf", "PR submission", or "pre-submit"
- User asks to fix reviewer feedback on a mathlib PR
- User wants to check code against mathlib conventions
- User asks "what's the project status?", "where are we stuck?", "what's the
  bottleneck?", "what's the worker doing?", "show me progress" → run `/project-status`

## Overview

This skill helps bring Lean 4 code up to mathlib standards by:
1. Enforcing style rules (line length, formatting, indentation)
2. Checking naming conventions
3. Ensuring proper documentation
4. Golfing proofs to be shorter and cleaner
5. Preparing code for PR submission

## Available Commands

| Command | Description |
|---------|-------------|
| `/develop` | **Planning only, with binding methodical-decomposition pre-work.** Phases 1a–1d: gather context, study references, search mathlib, design API. **Phase 1e (binding pre-work)**: for each top-level result, write the prose proof, decompose into ordered lemmas, **physically state every lemma as `:= by sorry` in the project's Lean files (Step 2.5 — skeleton must `lake build` clean)**, then tension against the references **with a verbatim source quote per leaf and a Lean ↔ source match paragraph (Step 3)**. Verify every leaf is discharged from mathlib (cited + verified) or already-developed project code — gaps become explicit API-gap sub-trees. Save `decomposition.md`. Only after every leaf is verified across (Lean declaration + verbatim quote + citation) does ticket creation (1g) proceed. Then ChatGPT validation (1h) and user approval (1i). Workers run via `/beastmode`. **Flag `--decompose`** runs ONLY Phase 1e and stops — for iterating on the skeleton / decomposition / source quotes before committing to a ticket board. |
| `/beastmode` | **Marathon execution. Stops at nothing — but stays on-target.** Pick a ticket, finish the goal no matter how deep the path goes. Spawn sub-tickets in `/develop`'s template format; replan via `/develop --continue` when a sketch is wrong; no recursion cap, no time budget. **Continuously checks on-target** before each sub-ticket and step (serves the plan? stays in the project's mathematical area? a refinement not a divergence?). **Welcomes scope growth that stays on target** — a "two lemmas" step turning into ten is great news, not a stop signal. Super Saiyan ethos: the harder the work, the more energy goes in. **Mandatory post-proof cleanup (Phase 6.5):** after gates pass and before mark-done, invokes `Skill(mathlib-quality:cleanup)` on every new declaration — full 10-phase workflow, no phase-skipping (enforced via /cleanup's own phase checklist); decompose flags spawn /decompose-proof sub-tickets, rename queue drained inside /cleanup's Phase 5b. Only stops: DONE / SCOPE-DEFINITION ERROR / OFF-TRACK (drift outside the project's mathematical scope, with concrete evidence) / BROKEN BASELINE. **"This is multi-session work" is NOT a stop** — it is the target signal. Beastmode exists to collapse multi-session work into one continuous run. |
| `/cleanup` | Style audit + cleanup + golf (whole file or single declaration). **9-phase methodical workflow**: doctor (baseline build) → prepare → audit punch-list → file-level fixes → per-declaration deep golf with diff gates → refactoring → final gates + cumulative checks → built-in `/simplify` pass → report. **Absorbed**: `/check-style` (Phase 2 audit), `/check-mathlib` (Phase 4 item 13 — five-method search + six strict rules + common-equivalents lookup), the inline mechanical pass of `/generalise` (Phase 4 item 18), and shouyi-style diff gates (Phase 4 + 6). Phase 6.5 hand-off to the built-in `/simplify` skill catches holistic issues the rule-driven pass missed. |
| `/cleanup-all` | **Orchestrator-worker pattern for project-wide cleanup.** Main session is the orchestrator: enumerates files, buckets by size, dispatches batched `Agent` calls with a ~1200-char verbatim prompt (working dir + branch + build + file list + target), narrates progress in one-line scoreboards between dispatches. Workers do the file reading, LSP, edits, Phase-4 sub-worker dispatch, and build verification in fresh contexts. Orchestrator never reads/edits/builds. The pattern that sustained a 28-day, 9000-message marathon. |
| `/decompose-proof` | Break long proofs into helper lemmas |
| `/overview` | **Project survey + per-decl mathlibable assessment.** Inventory + cross-file analyses (mathlib API audit, duplications, generalisation, missing API, junk) + **Step 9 Mathlibable Assessment**: pre-filters obvious SKIPs, then dispatches one `Skill(mathlib-quality:mathlibable)` per remaining public decl running the full 10-phase exhaustive workflow. Sequential with one-line scoreboard between. Per-decl detail reports go to `.mathlib-quality/overview/mathlibable/.md`. Writes `PROJECT_OVERVIEW.md` with per-bucket action lists. `--skip-mathlibable` for the faster draft view (all other steps). |
| `/project-status` | **Chat-only mathematical status.** The agent reads the project's `.lean` files (and `plan.md` / `tickets.md` if present) and reports in mathematical English: what result the worker is currently on, what (if anything) is blocked and what is 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. Tone is descriptive math reportage, not difficulty rhetoric. |
| `/expert-review` | Two-mode skill for external mathematical review. **Mode 1**: produce a self-contained `REVIEW_BRIEF.md` (no Lean, no file paths) — goals, plan, references, status, blockers, numbered questions — and stop, waiting for the reviewer's reply. **Mode 2** (`--reply`): once the reviewer responds, map their answers onto our questions, propose ticket/work-order updates, apply only after user approval. Session history persists in `.mathlib-quality/expert-review//`. |
| `/generalise` | Audit a lemma or definition for assumption weakening. Tries mechanical weakenings from a catalogue (typeclass parents, drop-unused, point-localise, strict→weak), then performs a literature search (WebSearch + ChatGPT MCP if available + mathlib's five-method search). Auto-applies small safe changes; presents big changes (public-API, restating, renames) as numbered options for user approval. |
| `/split-file` | Split large files (>1500 lines) into focused modules |
| `/pre-submit` | Pre-PR submission checklist |
| `/bump-mathlib` | Bump mathlib version and fix resulting breakage |
| `/mathlibable` | **Decide whether a Lean declaration belongs in mathlib.** Slow, methodical, ten-phase gated workflow with required artifacts per phase: doctor → comprehend → preliminary BIG/SMALL + one-line check (with defeq-abuse / diamond-avoidance / API-stability exemptions) → **EXHAUSTIVE literature search (always, every call — no `--quick` flag)**: WebSearch ×≥3 + ChatGPT MCP (with historical-formulation question) + local refs + nLab + nCatLab + Stacks + MathOverflow + arXiv → generality analysis vs literature-standard PLUS **Phase 4c modern-mathlib-idiom restatement (the Bourbaki 2.0 check)** asking whether contemporary mathlib tools (typeclasses, filters, universal properties, bundled types, module hierarchy, higher categories) would re-state with real downstream consequences → diamond/defeq risk assessment for `def`/`class`/`instance` → mathlib five-method search on user's form AND literature-standard AND modern-idiom forms → composition check (≤3 mathlib calls?) → verdict in one of five buckets (`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 (EXPENSIVE generalisations are explicitly worth doing). Phase-7 gate rejects unsupported verdicts, cost-based downgrades, and modern-idiom claims without concrete downstream consequences. **Mode A**: single declaration per call. **Mode B**: `/mathlibable ` or `/mathlibable   ...` — orchestrator-worker pattern dispatches one Agent per public decl sequentially, scoreboard between, writes `MATHLIBABLE_REPORT.md` aggregating verdicts. Also invoked from `/overview` Step 9 in the same way. Per-decl detail reports go to `.mathlib-quality/mathlibable/.md`. Bourbaki 2.0 philosophy + canonical modernisation cases + worked examples per bucket in `references/mathlibable-verdicts.md`. |
| `/blueprint` | **Author or update the project's verso-blueprint** — wraps [`leanprover/verso-blueprint`](https://github.com/leanprover/verso-blueprint) (the Verso-based tool behind verso-sphere-packing, verso-flt, verso-carleson). Chapter files are `.lean` modules under `/Chapters/`; statements are `:::theorem "label" (lean := "Foo.bar")` directives; dep-graph edges are `{uses "label"}[]`; math is KaTeX. Verso auto-computes completion status from `(lean := …)` — no manual `\leanok`. Seven-phase workflow (doctor → enumerate → plan → prose context → author → cross-link → hand-off). One worker per declaration; reads project references + module docstrings + `/develop`'s `decomposition.md` if present. Modes: whole-project default, single-file, `--decl ` (single-decl + closure, non-interactive), `--update`, `--check`, **`--migrate-from-latex []`** (one-shot mechanical 1:1 conversion of a legacy `leanblueprint` LaTeX tree). Phase 6 hand-off runs `./scripts/ci-pages.sh` and verifies `_out/site/html-multi/`. Conventions + Verso-specific deployment gotchas in `references/blueprint-conventions.md`. |
| `/unformalise` | **Turn one Lean declaration into mathematics.** Unicode terminal render by default (Γ, ℂ, ℍ, →, ≤ — readable in chat); after rendering, asks `[b]` add to blueprint as Verso / `[v]` Verso to stdout / `[m]` Markdown / `[n]` terminal-only. Non-interactive: `--verso`, `--md`, `--blueprint`. Single-decl default; `--closure` walks deps; whole-file mode also allowed. Shares the unformalisation worker logic with `/blueprint` Phase 4 (same `references/blueprint-conventions.md`). Conversational sibling to `/blueprint --decl`. |
| `/fix-pr-feedback` | Fetch PR comments, implement fixes locally, **wait for user approval before pushing**, then watch CI to completion. 8-phase workflow with explicit comment-coverage check. |
| `/setup-chatgpt` | Set up ChatGPT MCP server for mathematical second opinions |
| `/teach` | Teach the skill a project-specific pattern or convention |
| `/contribute` | Contribute local learnings back to the repo via PR |
| `/integrate-learnings` | (Maintainers) Process community contributions into reference docs |

## First-Time Setup

For mathematical second opinions from ChatGPT during formalization work, run `/setup-chatgpt`. This creates an MCP server that lets Claude Code query ChatGPT via the Codex CLI for proof strategies, Mathlib API hints, or verification of mathematical claims. Requires the ChatGPT desktop app and a Plus/Pro subscription.

## Core Style Rules (Quick Reference)

### File Structure
- **File names**: `UpperCamelCase.lean` (e.g., `TopologicalSpace.lean`)
- **Line length**: 100 characters max
- **File length**: 1500 lines max (MUST split if larger)
- **Proof length**: **50 lines absolute max** (target  1500 lines by theme
13. **Public helpers** - Helper lemmas should be `private` with `_aux` suffix
14. **Non-private internal lemmas** - Only export what other files need
15. **Long proofs (>50 lines)** - CRITICAL: decompose into helpers; target ` in statements / hypotheses** - Mathlib convention: every inequality in Lean code is `≤` / `` where natural — the rule is about Lean code.

## Deprecation Format

When renaming/removing public declarations, use:
```lean
@[deprecated (since := "YYYY-MM-DD")]
alias old_name := new_name

-- With explanation
@[deprecated "Use foo_bar instead" (since := "YYYY-MM-DD")]
theorem old_theorem ...
```
Deprecations can be removed after 6 months.

## Proof Decomposition

**Rule: No proof should exceed 50 lines. Target: main theorems 50 lines | **Critical - aggressive decomposition required** |

### The Decomposition Process (CRITICAL)

**This is a careful, systematic process. Do it right, not fast.**

#### Step 1: Identify Long Proofs
Scan the file and list ALL proofs >30 lines with their line numbers and counts.

#### Step 2: Understand the Complete Proof
Before touching any code, read the entire proof and answer:
1. What is the theorem proving (in plain language)?
2. What are the key mathematical steps in the argument?
3. What independent facts are being established?
4. What estimates/bounds appear?
5. Are there `cases`, `by_cases`, `rcases` that split into independent branches?
6. Are there repeated patterns across different proofs?

#### Step 3: Search Mathlib FIRST
**Before extracting ANY helper, search mathlib** to see if it already exists:
```
lean_loogle "Continuous → Bounded"           -- Type pattern search
lean_leansearch "continuous function on compact is bounded"  -- Natural language
lean_local_search "continuousOn_compact"     -- Local name search
```

Many "helper lemmas" are already in mathlib. Use them instead of writing new ones.

#### Step 4: Generalize Before Extracting
**CRITICAL: Don't create single-use helpers.** Before extracting, ask:
- Can this lemma be stated more generally?
- Would this be useful in other contexts?
- Are the hypotheses minimal, or tied to specific context?

```lean
-- BAD: Single-use helper tied to specific context
private lemma residue_theorem_step1 (γ : PiecewiseC1Curve) (S0 : Finset ℂ)
    (hγ_in_U : ∀ t ∈ Icc γ.a γ.b, γ.toFun t ∈ U) : ... := ...

-- GOOD: General lemma that could be useful elsewhere
lemma norm_sum_le_of_disjoint_balls {S : Finset ℂ} {ε : ℝ} (hε : 0  ... | inr => ...` or `by_cases`:
- Each case is often a standalone lemma
- Extract each case, then combine them in the main proof

```lean
-- Before: 80-line proof with two cases
theorem foo : P ∨ Q → R := by
  intro h
  cases h with
  | inl hp => ... 40 lines ...
  | inr hq => ... 40 lines ...

-- After: Two focused helpers + short main proof
private lemma foo_of_left (hp : P) : R := by ... 40 lines ...
private lemma foo_of_right (hq : Q) : R := by ... 40 lines ...

theorem foo : P ∨ Q → R := fun h => h.elim foo_of_left foo_of_right
```

#### Step 6: Check Definitions Too
Review ALL definitions in the file:
- Can they be simplified?
- Are they duplicating mathlib concepts?
- Should they use existing mathlib definitions instead?

### Decomposition Strategy
1. **Label sections by mathematical role**: setup, estimate, convergence, assembly
2. **Extract independent facts as helpers**: bounds, limits, constructions
3. **Name mathematically**: `norm_bound_of_continuous`, not `theorem_aux1`
4. **Minimize hypotheses**: weaker assumptions = more reusable lemmas
5. **Golf helpers aggressively**: isolated lemmas often become one-liners
6. **Consolidate shared logic**: same proof structure → parameterized helper
7. **Prefer mathlib**: if mathlib has it, use it; don't reinvent

### Helper Naming (Mathematical, not Structural)
```lean
-- Good: describes what it proves
private lemma norm_bound_of_continuous_on_compact : ...
private lemma limit_of_dominated_convergence : ...
lemma disjoint_balls_of_separated : ...  -- General, could be public

-- Bad: just references parent
private lemma big_theorem_aux1 : ...
private lemma step_2 : ...
```

### Helper Visibility
| Generality | Visibility |
|------------|------------|
| Very general, useful elsewhere | `lemma` (public) - consider if mathlib has it |
| Specific to this file's topic | `private lemma` |
| Only used once, can't generalize | `private lemma` with `_aux` suffix |

### Result
Main theorems should read as **clear outlines**:
```lean
private lemma continuity_bound : ‖f x‖ ≤ C := by ...
private lemma dominated_pointwise : ‖f_n x‖ ≤ g x := by ...

theorem main_result : ... :=
  limit_theorem (continuity_bound hf) (dominated_pointwise hg)
```

### Decomposition

…

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [CBirkbeck](https://github.com/CBirkbeck)
- **Source:** [CBirkbeck/mathlib-quality](https://github.com/CBirkbeck/mathlib-quality)
- **License:** MIT

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** no
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-cbirkbeck-mathlib-quality-mathlib-quality
- Seller: https://agentstack.voostack.com/s/cbirkbeck
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.