来源信息
- 仓库
- benbrastmckie/ModelChecker
- 最近来源活动
- 2026年3月4日 00:47
- 检测到的 SKILL.md 语言
- 英语
- 星标
- 13
- 分支
- 3
安装方式
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
检查来源文件
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
正在显示 SKILL.md
SKILL.md
来源说明 · 只读预览- name
- skill-lean-research
- description
- Research skill for Lean 4 theorem prover and Mathlib
- allowed_tools
- Read, Write, Edit, Bash, WebSearch, WebFetch, Grep, Glob, mcp__lean-lsp__*
- context
- project/lean4
# 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
在 GitHub 查看