openmath-lean-theorem
PassAudited by ClawScan on May 1, 2026.
Overview
This skill is coherent for setting up and checking Lean theorem workspaces, but users should notice that it can run local build commands and optionally install external Lean proof skills.
This appears safe to use for its stated Lean theorem workflow. Before installing or running auto-install, review the external leanprover/skills repository, use an explicit project-local install directory, and be aware that the preflight will run Lean/Lake build commands in the selected workspace.
Findings (2)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
Installing external skills can change what the agent is able to do in later Lean proof workflows.
The skill depends on external proof skills and can install them into a chosen skills directory. This is disclosed and purpose-aligned, but it is still third-party supply-chain behavior users should review.
External skills: Install required Lean proof skills from [leanprover/skills]... npx leanprover-skills install lean-proof ... preflight auto-install ... --install-dir .codex/skills
Review the leanprover/skills source before installing, prefer a project-local skills directory, and pin or verify versions where possible.
Running the preflight may download/build dependencies and execute the local project's build process.
The preflight workflow executes local Lean/Lake build commands inside the downloaded workspace. That is expected for theorem validation, but it can fetch dependencies and run project build logic.
If mathlib is required, runs: lake exe cache get ... Runs: lake build -q --log-level=info
Run it only in the intended OpenMath theorem workspace, inspect the generated lakefile/lean-toolchain when in doubt, and avoid using it on unrelated untrusted projects.