360 Secure SkillHub
360 安全技能中心

openmath-lean-theorem

该 Skill 假定定理工作区已由 openmath-open-theorem 创建，负责校验 lean、lake、elan 与工作区 lean-toolchain，安装外部 Lean 证明技能（lean-proof、mathlib-build），运行 scripts/check_theorem_env.py 做预检，并给出本地证明、lake build 验证的工作流指引；不包含定理下载、基准评…

bennyzhe
bennyzhe
热度 60.42
最近更新 2026-05-11 17:33:46
分类：开发依赖：代码执行 / 读写文件应用场景：代码生成 / 调试排错 / 研究 / 工作流

安装技能

复制下面的话术发给你的 Agent，它会通过 secure-skills 检索并安装该技能。

执行命令安装此 skill： npx secure-skills-cli add openmath-lean-theorem
Metadata
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

  • 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):