OpenMath Lean Theorem

---

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.0.2

requirements:

commands:

- python3

- lean

- lake

- elan

environment_variables:

- OPENMATH_SKILL_DIRS

- OPENMATH_LEAN_SKILL_INSTALL_DIR

- OPENMATH_LEAN_SKILL_REPO_URL

side_effects:

- May clone the reviewed leanprover/skills repo and copy missing Lean skills into an explicit install dir only when preflight is run with --auto-install-skills and --install-dir (or OPENMATH_LEAN_SKILL_INSTALL_DIR)

---

# 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.

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

```bash

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.

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

References

Load when needed (one level from this file):