研究检索需要联网clawhub未标认证来源可访问clear审计通过

openmath-open-theorem（openmath 开放定理）

Agent Skill

openmath-open-theorem 用于查找、检索和筛选相关信息，适合在 OpenClaw 中需要根据关键词、任务场景或来源线索快速定位候选结果时使用。可结合来源仓库、安装命令和原始 README 继续核验具体用法。安装前建议确认权限范围、维护状态，以及是否会触发联网、命令执行或文件读写。

总安装

8,470

周安装

346

GitHub Stars

公开资料未说明

下载量

2,713

OpenClaw

安装说明

本站只整理中文说明和来源信息，不托管安装包，也不代用户安装。

GitHub

来源数

许可证

MIT-0

最后核验

2026-05-01

来源状态

来源可访问

安装方式

通过对话安装

复制提示词发给支持本地命令或 Skills 的 AI 助手，先确认命令和权限，再让它执行。

请帮我安装这个 Agent Skill：openmath-open-theorem（openmath 开放定理）
来源仓库：https://github.com/bennyzhe/openmath-open-theorem
安装命令：
openclaw skills install openmath-open-theorem
安装前请先检查当前环境是否支持对应 CLI，并向我确认将要执行的命令、安装目录、联网范围和文件读写权限；确认后再执行。

命令行安装

复制命令到本机终端执行。该命令会通过 OpenClaw 从第三方来源获取 Skill；本站只展示命令，不托管安装包，也不自动执行。

ClawHubOpenClaw

openclaw skills install openmath-open-theorem

简介

openmath-open-theorem 用于查询从 OpenMath 平台打开的形式验证定理。

它支持获取 Lean 或 Rocq 特定定理列表，适合研究或教育用途。
通过 clawhub 安装，命令为 openclaw skills install openmath-open-theorem，需结合来源仓库和 README 核验具体用法。
安装前建议确认权限范围、维护状态，以及是否会触发联网、命令执行或文件读写操作。
适用于需要访问公开数学定理或形式化证明的用户。

SKILL.md

name: openmath-open-theorem
description: Queries open formal verification theorems from the OpenMath platform. Use when the user asks for a list of open theorems, wants Lean or Rocq-specific theorems, needs full detail for a theorem ID, or wants to download a theorem and scaffold a local proof workspace.
version: v1.0.0

OpenMath Open Theorem

Instructions

Query the OpenMath library to discover and scaffold open theorems. The discovery scripts use OPENMATH_SITE_URL and OPENMATH_API_HOST when set, and otherwise fall back to the default production endpoints.

First-run gate

Before discovery on a new machine or workspace, check the shared openmath-env.json. Auto-discovery only checks ./.openmath-skills/openmath-env.json and ~/.openmath-skills/openmath-env.json.

This gate is mandatory. If openmath-env.json is missing, or if it exists but preferred_language is missing, stop. Do not query the OpenMath theorem list, theorem detail, or download APIs until setup is complete.

If no config exists, stop and ask the user where to create it, then collect at least:

preferred_language: lean or rocq
config visibility / save scope: ./.openmath-skills or ~/.openmath-skills
the submit/authz fields only if the user wants end-to-end submission later

Command:

python3 scripts/check_openmath_env.py

Workflow checklist

[ ] Env: Run check_openmath_env.py. If openmath-env.json is missing from ./.openmath-skills and ~/.openmath-skills, or preferred_language is missing, ask the user to finish setup before continuing.
[ ] Explore: Run fetch_theorems.py [language] only after the first-run gate passes. If no language is passed, it uses preferred_language from openmath-env.json and must not fan out to other languages automatically.
[ ] Detail: Run fetch_theorem_detail.py <id> only after the first-run gate passes.
[ ] Download: Run download_theorem.py <id> only after the first-run gate passes.
[ ] Prove: Use the openmath-lean-theorem skill for environment setup, preflight checks, and proving.
[ ] Submit: Use the openmath-submit-theorem skill to hash and submit the proof.
[ ] Verify: Run fetch_theorem_detail.py <id> and confirm your address is the prover and status is verified.
[ ] Claim: Use the openmath-claim-reward skill to generate the withdrawal command.

Scripts

Script	Command	Use when
Shared env check	`python3 scripts/check_openmath_env.py [--config <path>]`	Mandatory first-run gate; validates shared config, preferred language, and the resolved OpenMath website/API endpoints.
List open theorems	`python3 scripts/fetch_theorems.py [--config <path>] [language]`	Listing or filtering open theorems after the first-run gate passes. `language`: optional `lean` or `rocq`. Without an explicit CLI language, query only the configured `preferred_language`.
Theorem detail	`python3 scripts/fetch_theorem_detail.py [--config <path>] <id>`	Need description, metadata, and formal definition (source) for a theorem ID; refuses to run until the first-run gate passes.
Download & scaffold	`python3 scripts/download_theorem.py [--config <path>] <id> [--output-dir <path>] [--force]`	Creating a local Lean or Rocq proof workspace after the first-run gate passes.

openmath_api.py is the shared API client. openmath_env_config.py reads shared user preferences from openmath-env.json.

Notes

Endpoints: Default website is https://openmath.shentu.org; default API host is https://openmath-be.shentu.org. Runtime overrides: OPENMATH_SITE_URL, OPENMATH_API_HOST.
Language: User-facing and API language naming is rocq.
No fallback: If preferred_language is lean, query only Lean by default. If no theorems are found, report that result and stop; do not automatically query Rocq, and vice versa.
Lean scaffold: Pins Lean and mathlib4 to v4.28.0. Rocq scaffold is _CoqProject-based.
After download: Use the openmath-lean-theorem skill for Lean environment setup, preflight, external skill installation, and the proving workflow.

References

Load when needed (one level from this file):

references/init-setup.md — Discovery-first setup flow for shared openmath-env.json, preferred language, and config visibility.
references/reward_overview.md — How rewards are calculated and how to claim them.

适合场景

OpenClaw 用户查找和安装 Skill 时

用户想查找某类 Agent Skill 时

需要根据任务场景推荐可安装能力包时

需要对比不同来源的安装命令和来源信息时

能力概览

能力 1

按任务关键词查找相关 Skills

能力 2

展示可复制的安装命令

能力 3

保留来源站点、仓库和原始说明，方便继续核验

能力 4

补充不同宿主或平台的使用分布数据

能力 5

展示第三方安全扫描或审计结果

安装后应在对应宿主中按原始 README 的触发条件使用；具体调用方式请以来源页面和 README 为准。

平台分布

OpenClaw

87.09%

按下载量换算2,363

安全审计

VirusTotal

通过

ClawScan

通过

Static analysis

通过

权限和风险

需要联网

该 Skill 可能需要联网访问来源站点、仓库或外部 API；具体网络访问范围需要结合源码和 README 复核。

安装前确认

本站仅展示第三方公开信息，不托管安装包，不提供自动安装或运行环境。安装前应自行审查源码、依赖和命令行为。当前只有一个来源，正式发布前建议补源仓库或其他目录站核验。

来源信息

GitHub 仓库

github.com

/bennyzhe/openmath-open-theorem

SKILL.md 来源

clawhub.ai

/bennyzhe/openmath-open-theorem

继续浏览同类 Skills

更多研究检索 Skills（73,675）返回 Skills 目录

上一个 Skill

openmath-claim-reward（openmath 领取奖励）

openmath-claim-reward 用于查找、检索和筛选相关信息，适合在 OpenClaw 中需要根据关键词、任务场景或来源线索快速定位候选结果时使用。可结合来源仓库、安装命令和原始 README 继续核验具体用法。安装前建议确认权限范围、维护状态，以及是否会触发联网、命令执行或文件读写。

下一个 Skill

openmath-submit-theorem（openmath 提交定理）

openmath-submit-theorem 用于查找、检索和筛选相关信息，适合在 OpenClaw 中需要根据关键词、任务场景或来源线索快速定位候选结果时使用。可结合来源仓库、安装命令和原始 README 继续核验具体用法。安装前建议确认权限范围、维护状态，以及是否会触发联网、命令执行或文件读写。