# mathlib-quality

A [Claude Code](https://docs.anthropic.com/en/docs/claude-code) skill plugin for developing, proving, cleaning up, and bringing Lean 4 code up to [mathlib](https://github.com/leanprover-community/mathlib4) 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`](https://github.com/CBirkbeck/MQSlim)

A [parallel slim plugin](https://github.com/CBirkbeck/MQSlim) 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