mathlib-quality

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 — Plan with /develop, then Execute with /beastmode

The development workflow is split into planning and execution to prevent the "agent reconsiders the whole approach mid-proof" failure mode. /develop does the strategic thinking; /beastmode does the tactical implementation; neither does the other's job.

/develop — planning only.

• Comprehensive plan from your references; exhaustive mathlib search; API design for every new declaration.
• Detailed self-contained tickets. Every proof/definition ticket contains the full Lean Statement, a numbered Proof Sketch citing sources, the Mathlib lemmas needed (verified to exist), the Sources with bibliographic info, and the Generality decision. Detailed enough that no replanning is needed once execution starts.
• Algorithmic cleanup-cadence: every 3 proof tickets per file → cleanup ticket; per-file finals; pre-milestone /cleanup-all; final-of-everything cleanup. The cadence is verified at planning time and re-checked at every resume audit.
• Resume & takeover modes: --continue audits the ticket board against the current code and proposes updates (including missing cleanup tickets); --takeover creates a plan for an existing project. Both end with a hand-off to /beastmode.
• No execution. Once the board is approved, /develop stops.

/beastmode — marathon execution. Stops at nothing — but stays on-target.

• Pick a ticket, finish the goal. No matter how deep the path goes. When a sub-step needs a missing lemma, missing dependency, or sub-result that isn't on the board, the worker spawns a sub-ticket in /develop's ticket-template format and immediately works it. When the parent's sketch turns out to be wrong as a strategy, the worker invokes /develop --continue to replan inline and keeps going.
• On-target vigilance, continuously. Before each sub-ticket and step, the worker confirms: serves the plan's main goal? stays in the project's mathematical area? a refinement, not a divergence? Vigilance is for on-target work, not against it.
• Scope growth that stays on-target is great news. A "two lemmas" step turning out to need ten is more mathematics captured — exactly the point of the marathon. The harder the work, the more energy goes in (Super Saiyan ethos: the stronger the opponent, the stronger you get).
• No recursion cap, no time budget. "It's late", "this is taking a while", "we're 5 sub-tickets deep", "let me try a different approach" — none of these are legitimate stops.
• Only legitimate stops: DONE / SCOPE-DEFINITION ERROR (statement actually wrong) / OFF-TRACK (drift onto material genuinely outside the project's mathematical area, with concrete evidence) / BROKEN BASELINE (lake build broken on entry).
• Quality enforced throughout — no sorry, no new axioms (#print axioms checked), maximum generality, gates run on the diff before marking the ticket done.

Clean Up Existing Code (/cleanup)

Methodical 8-phase workflow for any Lean file. Replaces what used to be three commands (/check-style, /check-mathlib, plus the original /cleanup):

• Phase 0 — Doctor: pre-flight lake build baseline check; aborts if the project doesn't currently compile (we can't tell what we broke without a clean baseline)
• Phase 2 — Style audit: full numbered punch-list; what was the standalone /check-style
• Phase 3 — File-level fixes: copyright + module docstring (CREATED if missing) + imports + subsection-divider strip + set_option removal + batched mechanical replacements
• Phase 4 — Per-declaration deep cleanup: one worker per decl; 18-item audit with required status blocks for golf rules (1.1 → 3.7), the five-method mathlib search (formerly /check-mathlib), and inline /generalise mechanical pass with literature search for public decls
• Phase 5 — Refactoring: cross-declaration items (renames, junk-def inlining, mathlib replacements, big-change generalisations escalated to standalone /generalise)
• Phase 6 — Final verification: file-level gates (definition_protected, theorem_statement_protected, lake_build_file, cumulative_no_unintended_breakage) — borrowed from shouyi
• One agent per declaration, deep focus on shortest proof; 60+ rules from golfing-rules.md and proof-patterns.md applied systematically (data-driven from 7,273 PR suggestions)

Additional Tools