mathlib

mathlib-claude-plugin

A Claude Code plugin that reviews Lean 4 / Mathlib code against community conventions.

What it does

/mathlib:review launches four parallel review agents that audit your changed .lean files:

Agent	Focus
Style & Naming	Line length, by placement, indentation, snake_case/UpperCamelCase, symbol dictionary, Type*
Documentation	Copyright headers, module docstrings, docBlame, section organization, import discipline
Proof Quality	Tactic selection (grind, gcongr, positivity), redundant sequences, @[simp]/@[ext] attributes, sorry detection
Generality	Type class assumptions (Ring vs Semiring), FunLike/SetLike patterns, simp normal form, API completeness

After all agents report, it fixes issues directly, runs lake exe runLinter and lake exe lint-style, and summarizes what changed.

Install

# Add the marketplace
/plugin marketplace add YOUR_GITHUB_USER/mathlib-claude-plugin

# Install the plugin
/plugin install mathlib@mathlib-tools

Or test locally without installing:

claude --plugin-dir ~/misc/mathlib-claude-plugin

Usage

In any Lean 4 / Mathlib project with uncommitted changes:

/mathlib:review

Sources

The review checklist is compiled from:

• Mathlib style guide
• Mathlib naming conventions
• Mathlib documentation guide
• Mathlib PR review criteria
• Zulip community discussions on linters, simp normal forms, and tactic conventions

License

Apache-2.0