openmath-lean-theorem

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.

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.

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.

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.

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.