By cbirkbeck
Prove, clean up, golf, and bring Lean 4 code up to mathlib standards
npx claudepluginhub cbirkbeck/mathlib-quality --plugin mathlib-qualityBump mathlib version and fix resulting breakage
Find mathlib equivalents to avoid duplication
Validate code against mathlib style rules
Run /cleanup on every file in the project, tracked file by file
Full file cleanup to mathlib standards
Contribute local learnings back to the mathlib-quality repo via PR
Break long proofs into helper lemmas
Plan and execute a mathematical development with ticket-based project management
Address PR reviewer comments
Process community learning contributions into reference docs and RAG index
Generate project declaration inventory for consolidation analysis
Pre-PR submission checklist
Set up the ChatGPT MCP server for mathematical second opinions
Set up the RAG MCP server for PR feedback search
Split large files (>1500 lines) into focused modules
Teach the skill a new pattern or project convention
Complete collection of battle-tested Claude Code configs from an Anthropic hackathon winner - agents, skills, hooks, rules, and legacy command shims evolved over 10+ months of intensive daily use
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.
/develop)The flagship command. Plans and executes a full mathematical development with:
/cleanup)Audit and golf declarations against mathlib standards:
grind, fun_prop, positivity, gcongr), term mode conversion, have inlining/plugin marketplace add CBirkbeck/mathlib-quality
/plugin install mathlib-quality
Also install the lean4-skills plugin, which provides the Lean 4 theorem proving workflows that mathlib-quality builds on:
/plugin marketplace add cameronfreer/lean4-skills
/plugin install lean4
git clone https://github.com/CBirkbeck/mathlib-quality.git
Then in Claude Code:
/plugin marketplace add /path/to/mathlib-quality
Nearly all commands (/develop, /cleanup, /decompose-proof, etc.) depend on
the lean-lsp-mcp server for sub-second
feedback instead of 30+ second lake build cycles. It provides tools like
lean_goal, lean_diagnostic_messages, lean_multi_attempt, lean_loogle, and more.
Prerequisites:
lakefile.leanlake build once in your project before starting (the LSP server needs oleans)Setup (run from your Lean project root):
# User-scoped (recommended) — available in all your projects
claude mcp add --transport stdio --scope user lean-lsp -- uvx lean-lsp-mcp
# Or project-scoped — shared via .mcp.json
claude mcp add --transport stdio --scope project lean-lsp -- uvx lean-lsp-mcp
User-scoped (--scope user) is recommended — it is more reliable for keeping MCP
tools visible inside subagents.
Restart Claude Code after adding. Verify by checking that tools like lean_goal
and lean_diagnostic_messages appear.
The plugin includes a searchable index of PR review examples. To enable:
/setup-rag
Get mathematical second opinions from ChatGPT during Lean 4 work. After setup,
Claude Code gains an ask_chatgpt_math tool for verifying claims, finding
Mathlib API hints, or getting unstuck on formalization problems.
Requirements:
Run the setup command and it will walk you through everything:
/setup-chatgpt
The command locates the Codex CLI, creates an MCP server at
~/.claude/mcp-servers/chatgpt-math/, installs dependencies, and adds the
server to your project's .mcp.json. Restart Claude Code after setup to
activate the new tool.
Complete collection of battle-tested Claude Code configs agents, skills, hooks, rules, and legacy command shims evolved over 10+ months of intensive daily use
Complete collection of battle-tested Claude Code configs from an Anthropic hackathon winner - agents, skills, hooks, and rules evolved over 10+ months of intensive daily use
20 SEO and GEO skills plus 15 commands on one shared operating contract. Includes protocol-layer gates for content quality, domain trust, entity truth, and campaign memory alongside keyword research, content creation, audits, monitoring, schema markup, and AI citation optimization. v9.0.0 adds legal/compliance hardening (FTC, GDPR, EU AI Act, WCAG), 10 new playbooks, SKILL.md size compliance (≤350 lines), native install for Gemini CLI / Qwen / Amp / Kimi / CodeBuddy, and the experimental /seo:geo-drift-check command.
Complete creative writing suite with 10 specialized agents covering the full writing process: research gathering, character development, story architecture, world-building, dialogue coaching, editing/review, outlining, content strategy, believability auditing, and prose style/voice analysis. Includes genre-specific guides, templates, and quality checklists.