openmath-lean-theorem

Compare original and translation side by side

🇺🇸

Original

English

🇨🇳

Translation

Chinese

OpenMath Lean Theorem

OpenMath Lean定理

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.

设置Lean证明环境，验证工具链，并在本地证明下载的OpenMath定理。假定定理工作区已由

openmath-open-theorem

技能创建。

本技能不运行基准测试提供程序、基于提示的Agent比较或轨迹持久化工作流。这些功能属于独立的

openmath-lean-benchmark

技能。

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

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.

环境：验证
```
lean
```
、
```
lake
```
和
```
elan
```
已安装，且与工作区的
```
lean-toolchain
```
版本匹配。
外部技能：从leanprover/skills安装所需的Lean证明技能。推荐手动安装：
bash
```
npx leanprover-skills install lean-proof
npx leanprover-skills install mathlib-build
```
如果你使用预检自动安装功能，请先查看上游仓库，然后传入明确的目标路径，例如
```
--install-dir .codex/skills
```
或
```
--install-dir .claude/skills
```
，以确保写入位置是你预期的。请勿在没有指定明确安装目录的情况下运行自动安装。
预检：运行
```
python3 scripts/check_theorem_env.py <workspace>
```
（参考references/preflight.md）。
证明：使用
```
lean-proof
```
/
```
mathlib-build
```
技能完成证明。关于OpenMath专属的证明循环，请参考references/proof_playbook.md。
验证：确认
```
lake build -q --log-level=info
```
执行通过，且没有剩余的
```
sorry
```
语句。
提交：使用
```
openmath-submit-theorem
```
技能对证明进行哈希处理并提交。

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.

脚本	命令	使用场景
预检检查	`python3 scripts/check_theorem_env.py <workspace>`	下载后、证明前运行；验证工具链、所需技能和初始构建状态。
自动预检	`python3 scripts/check_theorem_env.py <workspace> --auto-install-skills --install-dir <path>`	预检期间自动将缺失的Lean技能安装到指定的技能目录。

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.

Lean版本：脚手架固定使用

leanprover/lean4:v4.28.0

和

mathlib4 v4.28.0

（由

openmath-open-theorem

的

download_theorem.py

设置）。

外部技能：不随本工具打包。必备技能：
```
lean-proof
```
、
```
mathlib-build
```
。可选技能：
```
lean-mwe
```
、
```
lean-bisect
```
、
```
nightly-testing
```
、
```
mathlib-review
```
、
```
lean-setup
```
。推荐手动运行
```
npx leanprover-skills install ...
```
安装；预检自动安装额外需要
```
git
```
、明确的用户批准以及指定安装目录。
基准测试：如需对打包的Lean基准测试集进行Agent评估、提示比较或回归测试，请使用独立的
```
openmath-lean-benchmark
```
技能。

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.

按需加载（与本文件同级目录）：

references/preflight.md — Lean预检命令、技能检查和初始构建循环。
references/proof_playbook.md — 在本地证明已下载Lean定理的分步工作流。
references/languages.md — Lean版本和标准库说明。