Menu
The review-first prompt is selected by default. You can switch to a direct command or download a local copy.
Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.
Install with Codex or Claude Copy this prompt, paste it into Codex, Claude, or another assistant, and let it review the skill page and install it for you.
A direct command skips the review prompt. Inspect the source before running it.
npx skills add https://github.com/leanprover/skills --skill mathlib-buildThe command stays on one line. Scroll horizontally to inspect it before copying.
Prefer a local copy? Download the files currently available to SkillsMP.
Showing SKILL.md
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.
Based on SOC occupation classification
| name | mathlib-build |
| description | Building Mathlib |
Fetch the Mathlib olean cache before build:
lake exe cache get
Use lake exe cache get! (with !) to force re-download if the cache appears corrupt.
When building Mathlib reduce verbosity to save on tokens:
lake build -q --log-level=info
For merge conflict resolution or small fixes build only the affected files: lake build Mathlib.Foo.Bar -q --log-level=info.
Often it is fine to leave a complete build to CI. If you need a thorough local build, use lake build Mathlib MathlibTest Archive Counterexamples && lake exe runLinter.