openmath-open-theorem
v1.0.2Queries open formal verification theorems from the OpenMath platform. Use when the user asks for a list of open theorems, wants Lean or Rocq-specific theorem...
⭐ 0· 176·1 current·1 all-time
byshentu-org@bennyzhe
MIT-0
Download zip
LicenseMIT-0 · Free to use, modify, and redistribute. No attribution required.
Security Scan
OpenClaw
Benign
high confidencePurpose & Capability
Name/description (querying OpenMath, fetching details, scaffolding Lean/Coq workspaces) match the provided scripts (fetch_open_theorems, fetch_theorem_detail, download_theorem) and supporting config helpers. No unexpected credentials, binaries, or unrelated services are requested.
Instruction Scope
SKILL.md instructs the agent to run the included Python scripts and enforces a first-run gate that requires a local config file before contacting APIs. Scripts only read/write the declared config paths (.openmath-skills/openmath-env.json or ~/.openmath-skills/openmath-env.json), create scaffolds, and call the OpenMath API endpoints. There are no instructions to read unrelated system files or transmit data to unexpected endpoints (aside from allowed endpoint overrides).
Install Mechanism
This is an instruction-only skill (no install spec). Python scripts are bundled with the skill and executed locally; there are no external downloads or package installs specified. No high-risk installation behavior observed.
Credentials
No required environment variables or credentials are declared. The code respects optional overrides: OPENMATH_SITE_URL, OPENMATH_API_HOST, and OPENMATH_ENV_CONFIG — all are reasonable for endpoint/config overrides. These allow pointing to alternate API hosts, so users should avoid setting them to untrusted endpoints.
Persistence & Privilege
The skill is user-invocable and not forced always-on. It writes only to the project or user-scoped config directories it documents and generates local scaffold directories for downloaded theorems. It does not modify other skills or global agent settings.
Assessment
This skill appears to do what it says: it runs the bundled Python scripts to call OpenMath APIs and scaffold a local Lean/Coq project. Before installing/using it: (1) review the bundled scripts yourself (they will be executed locally by Python); (2) be aware the tool will create openmath-env.json under ./.openmath-skills or ~/.openmath-skills — choose project vs user scope appropriately; (3) the skill will make HTTP requests to the default hosts (https://openmath.shentu.org and https://openmath-be.shentu.org) or to any host you set via OPENMATH_API_HOST / OPENMATH_SITE_URL — do not override these to an untrusted endpoint; (4) no credentials are requested by default, but other skills (openmath-submit-theorem, openmath-claim-reward) are referenced for submission/claim workflows — inspect those before using end-to-end submission. Overall the package is coherent with its purpose.Like a lobster shell, security has layers — review code before you run it.
latestvk977agh9ay1ffkc1dpexh6w97583hbca
License
MIT-0
Free to use, modify, and redistribute. No attribution required.