Slim shadow of the mathlib-quality plugin. Same workflows (cleanup, mathlib-fit assessment, proof decomposition, project development, marathon execution) but trusts frontier-model judgement instead of over-specifying. Use when working with `.lean` files, mathlib contributions, proof golfing, or code review; or when the user types one of the `/clnup` / `/mthlbl` / `/devel` / `/bstmode` / `/decoproof` family of slash commands. Pair with the full mathlib-quality plugin to get both styles loaded; the user picks per task by typing `/cleanup` (verbose, defensively gated) vs `/clnup` (slim, trusts judgement).
2026-07-03