Menu
Use when preparing optional LeanExplore MCP setup for Lean declaration search and formalization support.
Installer avec Codex ou Claude Copiez ce prompt, collez-le dans Codex, Claude ou un autre assistant, puis laissez-le vérifier la page du skill et l'installer pour vous.
Basé sur la classification professionnelle SOC
Single-agent paper review workflow.
Comprehensive guide and reference for the Antigravity Customization System. Use to explain how customizations work, their loading priority, discovery mechanisms, and to guide the creation of skills, rules, plugins, hooks, and MCP servers.
Provides a comprehensive guide, quick reference, and sitemap for Google Antigravity (AGY), including the Antigravity CLI (agy), Antigravity 2.0, Antigravity IDE, Python SDK, slash commands, keybindings, and customizations (skills, rules, MCP, sidecars). Activate this skill when the user asks questions about how to use, configure, or customize Antigravity, AGY, the agy CLI, the Antigravity IDE, or Antigravity 2.0.
Guidelines for interacting with GitHub and request permissions from the user when commands fail due to restrictions in the agent environment.
ALWAYS use this skill when the user asks to send, get, retrieve, find, share, add, or search for a paper. This skill manages the user's Zotero library with 10,000+ papers and can retrieve PDFs, create share links, add new papers, and search. Prefer this over getscipapers for any request involving sending/getting/finding papers.
Use when the user asks to send, get, retrieve, find, share, add, or search for a paper. This is the live OpenClaw Zotero workflow adapted for Codex and should take priority over external paper retrieval.
| name | lean-explore-mcp |
| description | Use when preparing optional LeanExplore MCP setup for Lean declaration search and formalization support. |
This skill is installed as an OpenCode-native SKILL.md. For runtime-backed
helpers, prefer the shared ai-agents-skills runtime root and the
AAS_RUNTIME_ROOT override instead of assuming a Codex-specific runtime
path.
On native Windows, use the managed Windows runner and the native runtime command target. Set $runtime to the installed runtime root. Multi-agent installs usually use %LOCALAPPDATA%\ai-agents-skills\runtime. Then run:
$runtime = if ($env:AAS_RUNTIME_ROOT) { $env:AAS_RUNTIME_ROOT } else { "$env:LOCALAPPDATA\ai-agents-skills\runtime" }
& "$runtime\run_skill.bat" "skills/lean-explore-mcp/run_lean_explore_mcp.bat" doctor
PowerShell runner target:
& "$runtime\run_skill.ps1" "skills/lean-explore-mcp/run_lean_explore_mcp.ps1" doctor
POSIX examples below use run_skill.sh and .sh command targets; use the Windows command target above on native Windows.
Use this skill only for explicit optional LeanExplore MCP setup. It never installs packages, starts an MCP server, writes MCP/client config, stores credentials, downloads local data, or calls LeanExplore services. It reports local readiness and emits manual configuration snippets with placeholders.
Check local readiness without running lean-explore:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh doctor
Emit a manual MCP config snippet:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh config-snippet --backend api
Use --backend local only after local data has been prepared outside this repo with LeanExplore's own tooling.
Run offline smoke:
bash "$AAS_RUNTIME_ROOT/run_skill.sh" \
skills/lean-explore-mcp/run_lean_explore_mcp.sh smoke
The emitted local stdio snippet uses command lean-explore and args ["mcp", "serve", "--backend", "api"] or ["mcp", "serve", "--backend", "local"]. API mode uses placeholder LEANEXPLORE_API_KEY; local mode assumes a user-managed LeanExplore cache such as ~/.lean_explore/cache/.
LeanExplore output is Lean declaration retrieval evidence. Record it as lean_declaration_search, never as formal_check. It cannot set local lean_check_status, satisfy placeholder or trust-base scans, replace statement-equivalence review, or promote formal support without local Lean/project evidence.
When this skill is involved, consider these workflow templates (install via
the workflow-templates artifact profile, or --with-deps to pull backing skills):
informal-to-lean-formalization-runbook -- Local-first intake mapping an informal proof to Lean declarations with a scanner-first verification gate separating typecheck status from claim support.