openmath-lean-theorem

Configures Lean environments, installs external proof skills, runs preflight checks, and guides the workflow for proving downloaded OpenMath Lean theorems lo...

Security Scan

The skill's files and runtime instructions are coherent with its stated purpose (setting up and preflighting Lean theorem workspaces); nothing in the bundle requests unrelated credentials or attempts hidden exfiltration, though there are a few small notes about optional env vars and optional auto-install behavior you should understand before running it.

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.

Assessment

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.

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.

This skill does not run benchmark providers, prompt-based agent comparisons, or trace persistence workflows. Those belong to the separate openmath-lean-benchmark 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. Preferred manual install:

  npx leanprover-skills install lean-proof
  npx leanprover-skills install mathlib-build
  

  If you use preflight auto-install, first review the upstream repo and then pass an explicit target such as --install-dir .codex/skills or --install-dir .claude/skills so the write location is deliberate. Do not run auto-install without an explicit install dir.
• Preflight: Run python3 scripts/check_theorem_env.py <workspace> (see references/preflight.md).
• Prove: Use lean-proof / mathlib-build skills to complete the proof. See 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 additionally requires git, explicit user approval, and an explicit install 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 — Lean preflight command, skill checks, and initial build loop.
• references/proof_playbook.md — Step-by-step workflow for proving a downloaded Lean theorem locally.
• references/languages.md — Lean version and standard library.