lean-explore-cli

name	lean-explore-cli
description	Search Lean 4 / Mathlib declarations (theorems, definitions, lemmas, instances) by name or by informal meaning. Direct-CLI adapter for the OpenClaw sandbox (OpenClaw is not an MCP client, so this replaces the lean-explore MCP server).
user-invocable	true
disable-model-invocation	false
metadata	{"openclaw":{"requires":{"bins":"[Truncated]"}}}

Lean Explore (CLI)

Use this skill to search Lean 4 mathematical declarations from Mathlib and other packages — by declaration name (e.g. List.map, Nat.add) or by informal natural-language meaning (e.g. "a continuous function on a compact set", "prime number divisibility").

OpenClaw cannot use MCP servers, so this is a direct CLI wrapper around the lean_explore API (the same backend the LeanExplore MCP server uses).

Usage

exec: /workspace/skills/lean-explore-cli/run_lean_explore.sh search "<query>" [-n <limit>] [-p <package>]

• <query> — declaration name or natural-language description
• -n / --limit — number of results (default 5)
• -p / --package — restrict to a package (e.g. -p Mathlib); repeatable

Output is a single JSON object (results with declaration name, type, docstring, source link, etc.).

The runtime is supplied by the digest-locked sandbox image (or by the restored host Python closure when invoked outside the sandbox). The launcher never installs packages on use. The API key is read from the workspace secrets file; no key value is ever printed.

Examples

exec: /workspace/skills/lean-explore-cli/run_lean_explore.sh search "prime number divisibility" -n 3 -p Mathlib
exec: /workspace/skills/lean-explore-cli/run_lean_explore.sh search "List.map"

Readiness

exec: /workspace/skills/lean-explore-cli/run_lean_explore.sh doctor

Reports whether the venv/lean_explore are present and whether the API key is configured (auth_status: present|missing).