CBirkbeck

Mathlibable — Productivity skill for Claude Code

Productivity community

Decide whether a Lean declaration belongs in mathlib.

How to install Mathlibable

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.

What Mathlibable does

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

Alternatives in Productivity

Configure Claude HUD — FIRST: Use the Read tool to load ~/.claude/plugins/claude-hud/config.json if it exists 10.9k ★
GrokSearch — Integrate Grok's powerful real-time search capabilities into Claude via the MCP protocol 1.8k ★
🤝 Contributing To Agent Skills — First of all, thank you for taking the time to contribute 1.7k ★