⚡

// Skill profile

OpenMath Lean Theorem

Name: OpenMath Lean Theorem
Author: bennyzhe

name: openmath-lean-theorem

by bennyzhe · published 2026-04-01

开发工具自动化任务

Total installs

Stars

★ 0

Last updated

2026-04

// Install command

$ claw add gh:bennyzhe/bennyzhe-openmath-len-theorem

View on GitHub

// Full documentation

---

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.

// Comments

// Related skills

More tools from the same signal band

Order food/drinks (点餐) on an Android device paired as an OpenClaw node. Uses in-app menu and cart; add goods, view cart, submit order (demo, no real payment).

Sign plugins, rotate agent credentials without losing identity, and publicly attest to plugin behavior with verifiable claims and authenticated transfers.

The philosophical layer for AI agents. Maps behavior to Spinoza's 48 affects, calculates persistence scores, and generates geometric self-reports. Give your...

日历管理数据处理

1 installs★ 0