CBirkbeck

Mathlibable

Name: Mathlibable
Author: CBirkbeck

Productivity community

SOURCE https://github.com/CBirkbeck/mathlib-quality/blob/main/commands/mathlibable.md

Description

--- name: mathlibable description: Decide whether a Lean declaration belongs in mathlib. Methodical, gated workflow that combines thorough literature search (WebSearch + ChatGPT MCP + local references + nLab/Stacks/MathOverflow for big decls) with mathlib's five-method exhaustive search, then a generality analysis against the literature-standard form, then a composition check (can mathlib's primitives compose to give us this?), then synthesises a five-bucket verdict — YES-add-as-is | YES-but-gen

Installation

Installs to ~/.claude/skills/cbirkbeck-mathlib-quality-mathlibable/SKILL.md

Terminal

mkdir -p ~/.claude/skills/cbirkbeck-mathlib-quality-mathlibable && curl -fsSL https://raw.githubusercontent.com/CBirkbeck/mathlib-quality/HEAD/commands/mathlibable.md -o ~/.claude/skills/cbirkbeck-mathlib-quality-mathlibable/SKILL.md

Restart Claude Code, or start a new session, for it to be picked up.