# Skill Lean Research

> Research skill for Lean 4 theorem prover and Mathlib

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

---


# 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