openmath-open-theorem
Analysis
This skill appears purpose-aligned for querying OpenMath and creating local theorem scaffolds, with normal external API, local file-writing, and persistence considerations to review.
Findings (4)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
Checks for instructions or behavior that redirect the agent, misuse tools, execute unexpected code, cascade across systems, exploit user trust, or continue outside the intended task.
parser.add_argument("--force", action="store_true", help="Replace the target directory if it already exists."); ... shutil.rmtree(project_dir)The download helper can recursively replace the chosen output directory when --force is used. This is disclosed and not the default, but it is a local destructive capability users should handle carefully.
Source: unknown; Homepage: none; Required binaries (all must exist): none; No install spec — this is an instruction-only skill; Code file presence: 6 code file(s)
The artifacts include visible Python helper scripts but have limited provenance metadata and do not declare python3 as a required binary even though SKILL.md commands invoke it.
Checks for exposed credentials, poisoned memory or context, unclear communication boundaries, or sensitive data that could leave the user's control.
User | `~/.openmath-skills/openmath-env.json` | Reused across repositories
The setup flow can persist a preferred-language configuration globally, so future uses of the skill may be influenced by saved state outside the current repository.
theorem_code = theorem.theorem_code or ...; theorem_file.write_text(theorem_code.rstrip() + "\n", encoding="utf-8")
The skill writes remote theorem source from the OpenMath API into local Lean/Rocq files for later use. This is core to the purpose, but the downloaded content should be treated as untrusted until reviewed.