Skills openmath-lean-theorem

Name: openmath-lean-theorem
Author: openclaw

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

install

source · Clone the upstream repo

git clone https://github.com/openclaw/skills

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/openclaw/skills "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/bennyzhe/openmath-lean-theorem" ~/.claude/skills/openclaw-skills-openmath-lean-theorem && rm -rf "$T"

OpenClaw · Install into ~/.openclaw/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/openclaw/skills "$T" && mkdir -p ~/.openclaw/skills && cp -r "$T/skills/bennyzhe/openmath-lean-theorem" ~/.openclaw/skills/openclaw-skills-openmath-lean-theorem && rm -rf "$T"

manifest: skills/bennyzhe/openmath-lean-theorem/SKILL.md

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

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

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

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.