← 返回 Skills 市场
openmath-lean-theorem
作者
shentu-org
· GitHub ↗
· v1.0.3
· MIT-0
217
总下载
0
收藏
1
当前安装
3
版本数
在 OpenClaw 中安装
/install openmath-lean-theorem
功能描述
Configures Lean environments, installs external proof skills, runs preflight checks, and guides the workflow for proving downloaded OpenMath Lean theorems lo...
安全使用建议
This skill appears to do what it says: check your Lean workspace, verify toolchains, and (optionally) install missing proof skills. Before using auto-install: (1) prefer the manual 'npx leanprover-skills install ...' approach; (2) if you do use --auto-install-skills, always pass an explicit --install-dir (or set OPENMATH_LEAN_SKILL_INSTALL_DIR) and review the upstream repo (default: https://github.com/leanprover/skills.git); (3) be aware the script will probe common agent/skills directories under your home directory to detect installed skills; and (4) do not set OPENMATH_LEAN_SKILL_REPO_URL to an untrusted location unless you want to clone from it.
功能分析
Type: OpenClaw Skill
Name: openmath-lean-theorem
Version: 1.0.3
The skill bundle provides a legitimate environment for proving Lean theorems, including a preflight script (scripts/check_theorem_env.py) that validates toolchains and manages dependencies. While the script includes a capability to clone a remote repository (https://github.com/leanprover/skills.git) and install additional skills, this behavior is explicitly documented in SKILL.md as a side effect, requires opt-in flags (--auto-install-skills), and enforces the use of an explicit installation directory to prevent unauthorized modifications. The code uses safe subprocess handling, includes safety checks for directory creation, and lacks any indicators of data exfiltration, persistence, or malicious intent.
能力评估
Purpose & Capability
The skill name/description (configure Lean, run preflight, install proof skills) matches the provided assets: a SKILL.md describing preflight/install steps and a preflight Python script that detects toolchains, checks for required skills, optionally clones the official leanprover/skills repo, and runs build checks. Required binaries and actions (lean, lake, elan, python3, git for auto-install) are appropriate to the stated purpose.
Instruction Scope
Runtime instructions tell the agent to run a local preflight script which: inspects the workspace (files like lean-toolchain, lakefile.lean, theorem.json), searches common skill directories under the user's home and repo, optionally performs a lake build, and — only when --auto-install-skills plus an explicit install dir (or OPENMATH_LEAN_SKILL_INSTALL_DIR) are provided — clone the configured skill repo and copy missing skill directories into the chosen install dir. These steps are within scope for preparing a Lean proving environment, but they do touch the user's home-directory skill paths and will perform network cloning if the explicit auto-install path is used.
Install Mechanism
This is an instruction-only skill with an included Python script; there is no package install spec. The script may run 'git clone' of the DEFAULT_LEAN_SKILL_REPO_URL (default: https://github.com/leanprover/skills.git) into a temporary directory and copy selected skill subdirectories into an explicit install dir. Cloning a well-known GitHub repo is reasonable here, but the repo URL can be overridden via env var, so users should review the upstream repository before allowing auto-install.
Credentials
The registry shows no required env vars, but the SKILL.md and script use/recognize optional environment variables (OPENMATH_SKILL_DIRS, OPENMATH_LEAN_SKILL_INSTALL_DIR, OPENMATH_LEAN_SKILL_REPO_URL). Those are reasonable for customizing search/install locations. The script also enumerates and probes common skill directories under the user's home; this file-system inspection is expected for finding installed skills but is worth noting. No secrets or unrelated credentials are requested.
Persistence & Privilege
The skill is not always-enabled and does not request permanent platform privileges. It only writes files when the user explicitly runs the preflight with --auto-install-skills and supplies an explicit install directory (or sets OPENMATH_LEAN_SKILL_INSTALL_DIR). The script does not modify other skills' configs beyond copying selected skill directories into the user-specified target.
如何使用
- 确保已安装 OpenClaw（本地或 Docker 部署）
- 在对话框中输入安装命令：
/install openmath-lean-theorem - 安装完成后，直接呼叫该 Skill 的名称或使用
/openmath-lean-theorem触发 - 根据 Skill 的参数说明提供必要输入，即可获得结构化输出
版本历史
v1.0.3
Require explicit install dir for Lean preflight auto-install
v1.0.2
Require explicit install dir for Lean preflight auto-install
v1.0.0
Initial release of OpenMath Lean Theorem skill.
- Guides setup of Lean and associated toolchains for proving OpenMath theorems.
- Provides step-by-step workflow checklist, including environment verification, external skill installation, preflight checks, proof submission, and build verification.
- Supports LEAN4 benchmarking: setup, solve, check, validate, and analyze results with scoping options.
- Documents required and optional external Lean proof skills, along with links and installation steps.
- Includes references for detailed preflight, proof playbook, and benchmarking agent guides.
元数据
常见问题
openmath-lean-theorem 是什么？
Configures Lean environments, installs external proof skills, runs preflight checks, and guides the workflow for proving downloaded OpenMath Lean theorems lo... 它是一个面向 Claude Code / OpenClaw 的 AI Agent Skill 插件，目前累计下载 217 次。
如何安装 openmath-lean-theorem？
在 OpenClaw 或 Claude Code 对话框中运行命令「/install openmath-lean-theorem」即可一键安装，无需额外配置。
openmath-lean-theorem 是免费的吗？
是的，openmath-lean-theorem 完全免费，采用 MIT-0 许可证，可自由下载、安装和使用。
openmath-lean-theorem 支持哪些平台？
openmath-lean-theorem 跨平台运行，可在任意部署了 OpenClaw / Claude Code 的环境中使用（cross-platform）。
谁开发了 openmath-lean-theorem？
由 shentu-org（@bennyzhe）开发并维护，当前版本 v1.0.3。
推荐 Skills