leanprover

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.

Bisect 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.

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.

Retrieve and investigate failing Lean CI job logs. Use when a CI job fails and you need to fetch its logs, or when monitoring a CI run for failures.

Build and run tests against the stage2 Lean compiler. Use when asked to build, rebuild, or test against stage2.

Diagnose a spurious stage1 test failure caused by olean-persisted compiler changes. Use when a stage1 test fails unexpectedly and the change adds or modifies an environment extension or other information persisted into .olean files.

Write the Highlights section for Lean 4 release notes. Use when asked to write, draft, or update release highlights for a Lean version.

Profile Lean programs with demangled names using samply and Firefox Profiler. Use when the user asks to profile a Lean binary or investigate performance.

Extract Zulip thread HTML dumps into readable plain text. Use when the user provides a Zulip HTML file or asks to parse/read/convert/summarize a Zulip thread.

Use this when an AI should work on an external Lean project through the installed `lean-beam` wrapper, giving it direct efficient access to Lean's proof engine to avoid repeated inner-loop rebuilds through cheap speculative checks and zero-build module…

Use this when an AI needs the optional Rocq goal-probe surface exposed through the installed `lean-beam` wrapper while porting Rocq developments to Lean.

Restructures a Lean file with one or many solution implementations so that each solution is self-contained with its own Implementation, Tests, and Verification sections.

Performs thorough code reviews of individual human-eval problems. Use when asked explicity to review code or analyze code quality.

Lean 4 reference-counting and linearity: how to keep hot data structures unshared, diagnose copies, and avoid codegen traps

Work with Verso Blueprint Lean projects. Use when Codex needs to build or serve Blueprint HTML, query Blueprint labels/dependencies/owners/tags/work queues, debug generated graph/summary/preview data, inspect or edit Blueprint source modules, add conservative…