mathlib-quality

mathlib-quality

A Claude Code skill plugin for developing, proving, cleaning up, and bringing Lean 4 code up to mathlib standards.

Twenty-two commands spanning the whole workflow: plan → prove → cleanup → assess mathlib-fit → blueprint → self-review → PR. Every workflow is methodical, phase-numbered, and gated (missing artifacts fail the step); mathematical judgement is enforced through required evidence rather than through post-hoc review.

Sibling: MQSlim

A parallel slim plugin that shadows this one — same workflows, same load-bearing rails, restated in the "trust frontier- model judgement; minimal instructions" style Anthropic's skill-authoring guide explicitly recommends. Load both together and pick per task by typing /cleanup (verbose, gated) vs. /clnup (slim). MQSlim tests the hypothesis that frontier models produce better output when the prompts state the goal + the gates that catch real failures, and then get out of the way.

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.
• One conclusion per declaration. A result whose statement would bundle several independently-provable conclusions (a top-level ∧-chain, source parts (i)/(ii)/(iii)) is split at planning time — one lemma per part, each with its own name and minimal hypotheses; any kept bundle is a one-line ⟨…⟩ assembly. Long theorem statements never get born. Exceptions (shared-witness existentials, simultaneous-induction bundles) in references/statement-splitting.md.
• 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.
• Statements stay small (Tier A5). A ticket or would-be sub-ticket whose statement bundles several independently-provable conclusions is split before proving: one sub-ticket per part, then the bundled declaration is discharged as a one-line ⟨…⟩ assembly. Spawned sub-tickets are born single-conclusion.
• 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)