# Skill Lean Implementation

> Implementation skill for Lean 4 proofs and definitions

- Skill: `benbrastmckie/skill-lean-implementation-3` (Agent Skill)
- Install (CLI): `npx skillmds@latest add benbrastmckie/skill-lean-implementation-3`
- Raw SKILL.md: https://api.skillmd.com/api/skills/benbrastmckie/skill-lean-implementation-3/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: benbrastmckie (https://skillmd.com/u/benbrastmckie)
- Updated: 2026-09-21
- Page: https://skillmd.com/skills/benbrastmckie/skill-lean-implementation-3

---


# 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