lean-skills

Claude Code skills for building and auditing your own Lean 4 + Mathlib formalization: whether a statement means what it claims, and whether the prose citing it is still true. Tactic inventories, linter names, and error strings were extracted from the toolchain rather than recalled.

Seven skills, one per job. Topic-shaped skills fail in a specific way: a "tactics" skill and a "Mathlib" skill would both match every Lean task, so both would load, and neither would tell the agent what to do next. A task-shaped skill fires when its task comes up, and carries the workflow for it.

The failure the kernel doesn't catch

Two things go wrong in Lean work, and they fail independently.

The kernel catches the first: a proof that does not establish its statement will not compile. Nothing catches the second: a statement that does not mean what its author intended compiles perfectly and can sit in a library for years. x / 0 = 0 in Lean, so a theorem about a ratio is provable at a zero denominator for reasons that have nothing to do with the mathematics. These skills spend most of their length on that second failure, because it is the one you get no help with.

The other bias throughout is toward checking the toolchain on disk before trusting memory. Mathlib moves, and a model's recollection of it goes stale quietly. Two you can check yourself, at Mathlib v4.32.1:

• Mathlib/Tactic/Push.lean emits the warning `push_neg` has been deprecated. Prefer using `push Not` instead.
• The root-namespace div_add_div_same is gone. Only ENNReal.div_add_div_same survives — so a bare grep still returns a hit, and a model will still offer you the lemma that no longer applies.

Both are one grep away in .lake/packages/mathlib/. The skills say so repeatedly, and give the commands.

Installing

Symlink all seven into ~/.claude/skills/:

git clone https://github.com/matt-w-horn/lean-skills.git
cd lean-skills
mkdir -p ~/.claude/skills
for s in skills/*/; do
  ln -s "$PWD/$s" ~/.claude/skills/"$(basename "$s")"
done

For one skill, link it by name: ln -s "$PWD/skills/lean-proving" ~/.claude/skills/lean-proving.

Or install it as a Claude Code plugin. The owner/repo shorthand clones over SSH, so use the HTTPS URL unless you already have a GitHub key loaded in ssh-agent:

/plugin marketplace add https://github.com/matt-w-horn/lean-skills.git
/plugin install lean-skills@lean-skills

The shorthand /plugin marketplace add matt-w-horn/lean-skills works too, and setting CLAUDE_CODE_PLUGIN_PREFER_HTTPS=1 makes it clone over HTTPS as well.

To pull later changes, refresh the catalog and then the plugin:

/plugin marketplace update lean-skills
/plugin update lean-skills@lean-skills

Neither manifest sets a version, so every commit here is its own version and an update always has something to deliver. Third-party marketplaces have background auto-update off by default, so the two commands above are the manual path.

The loogle skill documents how to install the loogle binary. That install is optional: a hosted instance at https://loogle.lean-lang.org/ needs no install. Nothing else here has dependencies. The skills are Markdown. The only code is two standard-library Python tools, each with its tests: the validator in tools/ and the sweep renderer in the claims-review skill. CI runs the validator and both test suites.

Layout

skills/<name>/
├── SKILL.md        # the workflow, loaded when the skill fires
├── references/     # detail, loaded only when SKILL.md points at it
└── scripts/        # bundled tooling, where a skill has any

Only SKILL.md is required. lake and loogle are a single file each, and lean-claims-review is the one skill that bundles code.

The frontmatter is always in context, the body loads when the skill triggers, and reference files load only when SKILL.md points at them. Version-pinned inventories go to references/ for that reason: the tactic inventories, the error strings, and the linter list are long, and none of them should cost context on a task that never reaches for them. The validator enforces the other half of the bargain, failing CI on any file under references/ that no chain of mentions from SKILL.md reaches.

Sources

Written against Lean 4 and Mathlib at v4.32.0, with later additions checked at v4.32.1 — that is the toolchain the tactic inventories, linter names, and error strings were extracted from. Version-specific claims are marked, and the reference files that carry version-pinned inventories say how to regenerate them for a different pin.

Background reading drawn on: Theorem Proving in Lean 4, The Hitchhiker's Guide to Logical Verification, Logic and Proof, the Lean FAQ, Mathlib's naming conventions, and the 100 theorems tracking pages.

Related work

leanprover/skills is the Lean FRO's own skill set, aimed at contributing to Lean and Mathlib upstream: proof writing, MWE minimization, bisection, and PR conventions. cameronfreer/lean4-skills is a proving workflow pack with review and golf commands. This repository sits downstream of both, and most of its length goes to the checks nothing upstream covers. If you are contributing to Mathlib itself, start with the FRO's set.

Two sibling repositories put these skills to work. lean-self-audit-template is a fork-ready Lean 4 + Mathlib template whose claims ledger is the kind of project lean-claims-review referees. Overload is the formalization these skills were developed against, with every gate live.

Contributing

Corrections are welcome, particularly where a version-specific claim went stale. That is the failure mode this repository is most exposed to. python3 tools/validate_skills.py checks structure and cross-references, and runs in CI.

License

Apache-2.0. See LICENSE and NOTICE.