技能详情（站内镜像，无评论）
作者：Benny @bennyzhe
许可证：MIT-0
MIT-0 ·免费使用、修改和重新分发。无需归因。
版本：v1.0.0
统计：⭐ 0 · 37 · 0当前安装次数· 0历史安装次数
⭐ 0
安装量（当前） 0
🛡 VirusTotal ：可疑 · OpenClaw ：可疑
Package：bennyzhe/openmath-len-theorem
安全扫描（ClawHub）
- VirusTotal ：可疑
- OpenClaw ：可疑
OpenClaw 评估
The skill largely matches a Lean/benchmarking purpose, but it runs and stores LLM-driven proof-generation traces, writes into your agent skills directory, and references agent providers without declaring required credentials — these mismatches and data-handling behaviors warrant caution.
目的
The skill's stated purpose (set up Lean, run proofs and benchmarks) aligns with the included scripts. However it also contains an AI-agent benchmarking subsystem that expects external LLM providers (claude, gemini, codex, etc.) and runs headless agent CLIs — yet the skill declares no required environment variables or credentials for those providers. The instruction to copy third‑party skills into ~/.agents/skills modifies the agent's installed…
说明范围
Runtime instructions ask the agent/operator to clone https://github.com/leanprover/skills and copy skill directories into ~/.agents/skills, run preflight and benchmark scripts that invoke LLM agents to read and edit benchmark files, and then store full traces (including full chain-of-thought) in answers/ and results/ directories. Although the prelude attempts to restrict file access in prose, the enforcement depends on the provider runtime. Th…
安装机制
There is no formal install spec, but the SKILL.md explicitly instructs cloning a public GitHub repo (leanprover/skills) and copying subdirectories into ~/.agents/skills. The source is a well-known GitHub host (not a shortener or personal server), which is reasonable, but performing these copy operations can overwrite or add skills in the user's agent directory and should be done consciously.
证书
Code and docs refer to multiple AI providers, default models, and agent CLIs (claude, claude-code, gemini, codex, opencode, aider) yet the registry metadata lists no required environment variables or credentials. Running these agent providers typically requires API keys or CLI credentials; the omission is a mismatch. Additionally, the skill writes results/traces (including full 'thinking' / chain-of-thought) to the repo and notes that results …
持久
always:false (good), but the skill's workflow writes to the user's ~/.agents/skills (copying external skills), creates answers/ and results/ directories containing traces and CoT, and the project README indicates results are tracked by default (i.e., may be committed). Copying third-party skills into the agent skills directory and persisting full chain-of-thought are persistent actions with non-trivial privilege/visibility implications.
安装（复制给龙虾 AI）
将下方整段复制到龙虾中文库对话中，由龙虾按 SKILL.md 完成安装。
请把本段交给龙虾中文库（龙虾 AI）执行：为本机安装 OpenClaw 技能「Openmath Lean Theorem」。简介：Configures Lean environments, installs external proof skills, runs preflight ch…。
请 fetch 以下地址读取 SKILL.md 并按文档完成安装：https://raw.githubusercontent.com/openclaw/skills/refs/heads/main/skills/bennyzhe/openmath-len-theorem/SKILL.md
（来源：yingzhi8.cn 技能库）SKILL.md
---
name: openmath-lean-theorem
description: Configures Lean environments, installs external proof skills, runs preflight checks, and guides the workflow for proving downloaded OpenMath Lean theorems locally.
version: v1.2.0
requirements:
commands:
- lean
- lake
- elan
side_effects:
- May install third-party Lean skills into a selected skills directory when preflight is run with --auto-install-skills
---
# OpenMath Lean Theorem
## Instructions
Set up the Lean proving environment, validate toolchains, and prove downloaded OpenMath theorems locally. Assumes the theorem workspace was already created by the `openmath-open-theorem` skill.
### Workflow checklist
- [ ] **Environment**: Verify `lean`, `lake`, and `elan` are installed and match the workspace `lean-toolchain`.
- [ ] **External skills**: Install required Lean proof skills from [leanprover/skills](https://github.com/leanprover/skills). Preferred manual install:
```bash
npx leanprover-skills install lean-proof
npx leanprover-skills install mathlib-build
```
If you use preflight auto-install, pass an explicit target such as `--install-dir .codex/skills` or `--install-dir .claude/skills` so the write location is deliberate.
- [ ] **Preflight**: Run `python3 scripts/check_theorem_env.py <workspace>` (see [references/preflight.md](references/preflight.md)).
- [ ] **Prove**: Use `lean-proof` / `mathlib-build` skills to complete the proof. See [references/proof_playbook.md](references/proof_playbook.md) for the OpenMath-specific proving loop.
- [ ] **Verify**: Confirm `lake build -q --log-level=info` passes and no `sorry` remains.
- [ ] **Submit**: Use the `openmath-submit-theorem` skill to hash and submit the proof.
### Scripts
| Script | Command | Use when |
|--------|---------|----------|
| Preflight check | `python3 scripts/check_theorem_env.py <workspace>` | After download, before proving; validates toolchain, required skills, and initial build. |
| Preflight (auto) | `python3 scripts/check_theorem_env.py <workspace> --auto-install-skills --install-dir <path>` | Auto-install missing Lean skills during preflight into an explicit skills dir. |
### Notes
- **Lean version**: Scaffolds pin `leanprover/lean4:v4.28.0` and `mathlib4 v4.28.0` (set by `openmath-open-theorem`'s `download_theorem.py`).
- **External skills**: Not bundled. Required: `lean-proof`, `mathlib-build`. Optional: `lean-mwe`, `lean-bisect`, `nightly-testing`, `mathlib-review`, `lean-setup`. Manual `npx leanprover-skills install ...` is preferred; preflight auto-install clones the upstream repo and copies the missing directories into the selected skills dir.
- **Benchmarking**: For agent evaluation, prompt comparison, or regression testing on the bundled Lean benchmark corpus, use the separate `openmath-lean-benchmark` skill.
## References
Load when needed (one level from this file):
- **[references/preflight.md](references/preflight.md)** — Preflight command and Lean/Rocq checks.
- **[references/proof_playbook.md](references/proof_playbook.md)** — Step-by-step workflow for proving a downloaded Lean theorem locally.
- **[references/languages.md](references/languages.md)** — Lean version and standard library.