mathlib-quality-plugins

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:

1. Plan -- asks for your goal and references, searches mathlib exhaustively, designs API, creates ticket board with dependency graph
2. Execute -- dispatches one worker per ticket; each searches mathlib, drafts statements, proves via multi-cycle approach, decomposes proofs >50 lines
3. Enforce -- no sorry placeholders, no new axioms (#print axioms checked), maximum generality, periodic /cleanup passes
4. 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:

1. Runs 13-item audit (lint, have scan, simp squeeze, naming, line packing, ...)
2. Applies 30+ golfing rules (instant wins + automation upgrades)
3. Steps back to think holistically about the shortest possible proof
4. 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