skill-lean-implementation
Implementation skill for Lean 4 proofs and definitions
Source facts
- Repository
- benbrastmckie/ModelChecker
- Last source activity
- March 4, 2026 at 00:47
- Detected SKILL.md language
- English
- Stars
- 14
- Forks
- 3
Install options
The review-first prompt is selected by default. You can switch to a direct command or download a local copy.
Review the source files
Read SKILL.md and any companion files shown by SkillsMP before deciding whether to install.
Showing SKILL.md
SKILL.md
Source instructions · Read-only preview- name
- skill-lean-implementation
- description
- Implementation skill for Lean 4 proofs and definitions
- allowed_tools
- Read, Write, Edit, Bash, Grep, Glob, mcp__lean-lsp__*
- context
- project/lean4
# Lean Implementation Skill
Routes Lean 4 implementation tasks to lean-implementation-agent.
## Usage
Invoked by orchestrator when task language is `lean4` and operation is implementation.
## Agent
- **Agent**: lean-implementation-agent
- **Model**: default
## Context
- Lean 4 tactic patterns
- Proof structure templates
- MCP tools for proof assistance
View on GitHub