Stats
Actions
Tags
Help us improve
Share bugs, ideas, or general feedback.
From lean
Creates minimal working examples (MWEs) from Lean 4 errors for bug reports using lake minimizers, with setup for lean4 and mathlib4 repositories.
npx claudepluginhub leanprover/skills --plugin leanHow this skill is triggered — by the user, by Claude, or both
Slash command
/lean:lean-mweThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
1. **Set up the guard** (`#guard_msgs` or `#guard_panic`)
Bisects Lean 4 toolchain commits to identify regressions or behavior changes using self-contained test file signatures. Useful for Lean 4 debugging.
Assists with Lean 4 theorem proving: editing .lean files, debugging builds (type mismatches, sorries, axioms, lake errors), searching mathlib lemmas, formalizing mathematics, and learning concepts via commands like /lean4:prove and /lean4:formalize.
Enforces mathlib code quality and style for Lean 4, including formatting, naming conventions, documentation, and proof golfing. Useful when preparing a PR or fixing reviewer feedback.
Share bugs, ideas, or general feedback.
#guard_msgs or #guard_panic)lake exe minimizeFor Mathlib-related bugs:
cd /tmp
git clone https://github.com/kim-em/mathlib-minimizer.git
cd mathlib-minimizer
lake exe cache get
For pure Lean 4 bugs:
cd /tmp
git clone https://github.com/kim-em/lean-minimizer.git
cd lean-minimizer
Use #guard_msgs to capture the exact error:
import Mathlib.SomeModule
/--
error: the exact error message
goes here verbatim
-/
#guard_msgs in
example : ... := by some_tactic
import Mathlib.SomeModule
#guard_msgs in
#guard_panic in
some_command_that_panics
lake env lean YourFile.lean
No output = success (guard passed). Error output = guard failed, and you need to redesign the test case.
lake exe minimize YourFile.lean
Output is written to YourFile.out.lean.
--resume: Continue from the output file if interrupted--quiet: Suppress progress output--only-delete: Only run the deletion pass--only-import-inlining: Only inline importsNever use --no-import-inlining. The entire point is to produce a self-contained file.
Use --resume to continue from where you left off:
# Initial run (Ctrl-C if needed)
lake exe minimize YourFile.lean
# Resume later
lake exe minimize YourFile.lean --resume
After manually editing the .out.lean file, always use --resume to continue from the edited state.
lake env lean YourFile.out.lean
.out.lean file compiles with the expected error/panic#guard_msgs matches exactly