Skill Lean Implementation

Implementation skill for Lean 4 proofs and definitions

benbrastmckie Updated

File contents

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

benbrastmckie/modelchecker/tree/main/.opencode/skills/skill-lean-implementation commit 87204f71b0

Frequently asked questions

npx skillmds@latest add benbrastmckie/skill-lean-implementation-3