By leanprover
Streamline Lean 4 and Mathlib development: set up toolchains with elan and lake, bisect regressions in self-contained tests, generate minimal error examples for bug reports, enforce and review PR conventions, receive tactic-by-tactic proof guidance, optimize quiet builds with olean cache, and investigate nightly CI failures.
npx claudepluginhub leanprover/skills --plugin leanBisect Lean toolchain versions to find where behavior changes. Use when trying to identify which Lean 4 commit caused a regression or behavior change.
Create minimal working examples (MWEs) from Lean errors for bug reports. Use when minimizing a Lean error, creating an MWE, or preparing a bug report for lean4 or mathlib4.
PR conventions for the leanprover/lean4 repository. Use when creating pull requests, writing commit messages, or following project conventions for Lean contributions.
Use when asked to prove something in Lean. Covers one-step-at-a-time proving, error priority, working on the hardest case first, proof cleanup, and handling dependent type rewriting issues.
Set up a lean4 repository clone with proper elan toolchains.
Building Mathlib
PR conventions for leanprover-community/mathlib4. Use when creating pull requests, writing commit messages, or managing labels for Mathlib contributions.
Review guidelines for Mathlib PRs. Use when reviewing pull requests, checking code quality, or assessing whether a PR is ready to merge.
Understanding the Lean/Mathlib nightly testing infrastructure. Use when working on toolchain bumps, adaptation PRs, or investigating nightly CI failures.
Official Agent Skills for developing with Lean 4.
These skills help AI coding agents work effectively with Lean 4 code — writing proofs, setting up development environments, debugging toolchain regressions, and following project conventions.
| Skill | Description |
|---|---|
lean-proof | Writing Lean proofs: one step at a time, error priority, hardest case first |
lean-setup | Setting up a lean4 development environment with elan toolchains |
lean-bisect | Bisecting Lean toolchain versions to find regressions |
lean-mwe | Creating minimal working examples for bug reports |
lean-pr | PR conventions for the lean4 repository |
mathlib-build | Building Mathlib with appropriate verbosity settings |
mathlib-pr | PR conventions for Mathlib: labels, merge process, queueboard |
mathlib-review | Review guidelines for Mathlib PRs: tools, attributes, style checks |
nightly-testing | Understanding the Lean/Mathlib nightly testing infrastructure |
In Claude Code, type /plugin, under "Marketplaces" add "https://github.com/leanprover/skills.git", then under "Plugins" install the lean plugin.
Or in a terminal
claude plugin marketplace add https://github.com/leanprover/skills.git
claude plugin install lean@leanprover
gemini skills install https://github.com/leanprover/skills --path skills
Inside a Codex session:
$skill-installer install https://github.com/leanprover/skills/tree/main/skills/*
Or clone and copy the skills:
git clone https://github.com/leanprover/skills.git /tmp/lean-skills
cp -r /tmp/lean-skills/skills/* ~/.codex/skills/
Clone this repository and point your tool at the skills/ directory.
Every skill should be validated by test cases that demonstrate it actually improves agent performance. As base model capabilities increase over time, skills that no longer provide value can be identified and removed.
Each test case is a YAML file in skills/<name>/tests/ specifying a git repo, commit SHA, and prompt. Test infrastructure and results live in a separate repository: leanprover/skills-testing.
# Check that all skills have current satisfactory results
scripts/check-validation
# Check a specific skill
scripts/check-validation lean-proof
This is also run in CI on every push and pull request.
Clone the testing repo into this directory (it's gitignored):
git clone https://github.com/leanprover/skills-testing.git
Then run tests:
# Run all tests for a skill
skills-testing/scripts/run-skill-tests lean-proof
# Judge completed runs
skills-testing/scripts/judge-all
# View results
skills-testing/scripts/summary --latest
Commit results back to skills-testing so CI passes.
repo: "https://github.com/owner/repo.git"
sha: "abc123"
prompt: |
Your prompt here.
description: "What this tests"
# Optional: subdirectory, claude_flags, timeout (default 600s)
Apache-2.0
Access thousands of AI prompts and skills directly in your AI coding assistant. Search prompts, discover skills, save your own, and improve prompts with AI.
Behavioral guidelines to reduce common LLM coding mistakes, derived from Andrej Karpathy's observations on LLM coding pitfalls
Comprehensive skill pack with 66 specialized skills for full-stack developers: 12 language experts (Python, TypeScript, Go, Rust, C++, Swift, Kotlin, C#, PHP, Java, SQL, JavaScript), 10 backend frameworks, 6 frontend/mobile, plus infrastructure, DevOps, security, and testing. Features progressive disclosure architecture for 50% faster loading.
Design fluency for frontend development. 1 skill with 23 commands (/impeccable polish, /impeccable audit, /impeccable critique, etc.) and curated anti-pattern detection.
Reliable automation, in-depth debugging, and performance analysis in Chrome using Chrome DevTools and Puppeteer
Claude Code skills for Godot 4.x game development - GDScript patterns, interactive MCP workflows, scene design, and shaders