Skill Lean Research

Research skill for Lean 4 theorem prover and Mathlib

benbrastmckie Updated

File contents

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

benbrastmckie/modelchecker/tree/main/.opencode/skills/skill-lean-research commit 35db99cbdc

Frequently asked questions

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