mathlib-quality
A Claude Code skill plugin for developing, proving, cleaning up, and bringing Lean 4 code up to mathlib standards.
Built on 14,000+ real mathlib PR review comments with 7,273 before/after code suggestions, extracted into concrete golfing rules and quality principles.
What It Does
Develop New Mathematics (/develop)
The flagship command. Plans and executes a full mathematical development with:
- Project planning -- creates a comprehensive plan from your references, searches mathlib exhaustively, designs API for every new definition
- Ticket management -- breaks work into trackable tickets with dependencies, parallel capacity, and proof sketches
- Focused workers -- one agent per ticket, deep focus on finding the cleanest proof possible
- Resume & takeover -- pick up where you left off, or take over an existing project with full audit
- Quality enforced throughout -- no sorry placeholders, no new axioms, 50-line proof limit with auto-decomposition, periodic cleanup passes
- Maximum generality -- always prove in the most general setting, never take shortcuts
Clean Up Existing Code (/cleanup)
Audit and golf declarations against mathlib standards:
- 13-item audit per declaration (lint, have scan, simp squeeze, naming, structure, mathlib check, ...)
- 30+ golfing rules applied systematically (data-driven from 7,273 PR suggestions)
- One agent per declaration with deep focus on shortest proof
- Works on a whole file or a single declaration
Additional Tools
- Golf proofs -- automation upgrades (
grind, fun_prop, positivity, gcongr), term mode conversion, have inlining
- Decompose long proofs -- break proofs >30 lines into focused helper lemmas
- Check for mathlib duplication -- search mathlib before writing new definitions
- Prepare PRs -- comprehensive pre-submission checklist
- Fix reviewer feedback -- parse and address PR review comments
Installation
Option 1: Claude Code Plugin
/plugin marketplace add CBirkbeck/mathlib-quality
/plugin install mathlib-quality
Option 2: Local Clone
git clone https://github.com/CBirkbeck/mathlib-quality.git
Then in Claude Code:
/plugin marketplace add /path/to/mathlib-quality
Optional: RAG MCP Server
The plugin includes a searchable index of PR review examples. To enable:
/setup-rag
Commands
| Command | Description |
|---|
/develop | Plan and execute a mathematical development with ticket management |
/cleanup | Audit + golf (whole file or single declaration) |
/cleanup-all | Run /cleanup on every file in the project |
/check-style | Validate code against style rules (non-destructive) |
/decompose-proof | Break long proofs into helper lemmas |
/check-mathlib | Find mathlib equivalents to avoid duplication |
/pre-submit | Pre-PR submission checklist |
/fix-pr-feedback | Address PR reviewer comments |
/bump-mathlib | Bump mathlib version and fix breakage |
/setup-rag | Configure the RAG MCP server |
Usage
Developing New Mathematics
/develop # Start a new development (plan, tickets, prove)
/develop --continue # Resume from existing tickets
/develop --status # Show current ticket board
/develop --takeover # Take over an existing project
How /develop works:
- Plan -- asks for your goal and references, searches mathlib exhaustively, designs API, creates ticket board with dependency graph
- Execute -- dispatches one worker per ticket; each searches mathlib, drafts statements, proves via multi-cycle approach, decomposes proofs >50 lines
- Enforce -- no sorry placeholders, no new axioms (
#print axioms checked), maximum generality, periodic /cleanup passes
- Resume -- on restart, deep-scans project state, cross-references tickets with reality, updates plan with user
Cleaning Up Code
/cleanup MyFile.lean # Clean entire file
/cleanup MyFile.lean theorem_name # Clean one declaration
/cleanup-all # Clean every file in project
How /cleanup works:
For each declaration, a dedicated agent:
- Runs 13-item audit (lint, have scan, simp squeeze, naming, line packing, ...)
- Applies 30+ golfing rules (instant wins + automation upgrades)
- Steps back to think holistically about the shortest possible proof
- Verifies compilation
Preparing a PR
/check-style MyFile.lean # Check style (non-destructive)
/cleanup MyFile.lean # Fix everything
/pre-submit MyFile.lean # Final checklist
Handling PR Feedback
/fix-pr-feedback 1234 # Process feedback from PR #1234
/fix-pr-feedback --comments "..." # Or paste specific comments
CBirkbeck