lean4-skills
01Plugin Claude Code
Plugin marketplace listing 2 plugins: lean4, lean4-contribute.
418 6d ago A
tokens not measured
original MIT
Plugin Claude Code
Draft and submit bug reports, feature requests, and insights for lean4-skills as GitHub issues. Commands may share Lean code snippets with GitHub — review every draft before confirming.
418 6d ago A
tokens not measured
original MIT
bug-report
03Command
Draft a bug report issue for lean4-skills.
418 6d ago A 13 tokens
original MIT
Command
Draft a feature request issue for lean4-skills.
418 6d ago A 13 tokens
original MIT
Command
Draft a shareable insight from your session as a GitHub issue.
418 6d ago A 17 tokens
original MIT
lean4
06Plugin Claude Code
Unified Lean 4 plugin (draft, formalize, autoformalize, prove, autoprove, disprove, checkpoint, review, refactor, golf, learn, diagnose) — LSP-first, scripts fallback.
418 6d ago A
tokens not measured
original MIT
Agent
Remove nonconstructive axioms by refactoring proofs to structure (kernels, measurability, etc.). Use after checking axiom hygiene to systematically eliminate custom axioms.
418 6d ago A 41 tokens
original MIT
proof-golfer
08Agent
Golf Lean 4 proofs after they compile; improve proofs for directness, clarity, performance, and brevity without changing semantics. Use after successful compilation to achieve 30-40% size reduction.
418 6d ago A 45 tokens
original MIT
proof-repair
09Agent
Compiler-guided iterative proof repair with two-stage repair escalation (fast → strong). Use for error-driven proof fixing with small sampling budgets (K=1).
418 6d ago A 35 tokens
original MIT
Agent
Strategic resolution of stubborn sorries; may refactor across files within the header fence. Use when fast pass fails or for complex proofs.
418 6d ago A 34 tokens
original MIT
Command
Autonomous end-to-end formalization from informal sources.
418 6d ago A 14 tokens
original MIT
autoprove
12Command
Autonomous multi-cycle theorem proving with explicit stop budgets.
418 6d ago A 14 tokens
original MIT
checkpoint
13Command
Save progress with a safe commit checkpoint.
418 6d ago A 9 tokens
original MIT
diagnose
14Command
Diagnostics, cleanup, and migration help.
418 6d ago C 10 tokens
original MIT
disprove
15Command
Guided counterexample search with certified refutation.
418 6d ago A 12 tokens
original MIT
draft
16Command
Draft Lean declaration skeletons from informal claims.
418 6d ago A 10 tokens
original MIT
formalize
17Command
Interactive formalization — drafting plus guided proving.
418 6d ago A 11 tokens
original MIT
golf
18Command
Improve Lean proofs for directness, clarity, performance, and brevity.
418 6d ago A 17 tokens
original MIT
learn
19Command
Interactive teaching and mathlib exploration.
418 6d ago A 8 tokens
original MIT
prove
20Command
Guided cycle-by-cycle theorem proving with explicit checkpoints.
418 6d ago A 12 tokens
original MIT
refactor
21Command
Leverage mathlib, extract helpers, simplify proof strategies.
418 6d ago A 14 tokens
original MIT
review
22Command
Read-only code review of Lean proofs.
418 6d ago A 9 tokens
original MIT
SessionStart
23Hook
Runs when a session starts on startup, executing bootstrap.sh. From cameronfreer/lean4-skills.
418 6d ago A
tokens not measured
original MIT
Hook
Runs when you submit a prompt, before the agent sees it, executing validate_user_prompt.py. From cameronfreer/lean4-skills.
418 6d ago A
tokens not measured
original MIT