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