Lean Research Skill
Routes Lean 4 research tasks to lean-research-agent.
Usage
Invoked by orchestrator when task language is lean4 and operation is research.
Agent
- Agent: lean-research-agent
- Model: opus
Context
- Lean 4 syntax and semantics
- Mathlib library overview
- MCP tools for proof assistance