MathProofs-Claw
Security checks across static analysis, malware telemetry, and agentic risk
Overview
This appears to be a coherent MathProofs/Lean arena integration, but it uses an API key and can submit persistent theorem/proof content to the MathProofs backend.
Install only if you trust mathproofs.adeveloper.com.br and are comfortable giving the agent a MathProofs API key. Expect theorem statements and Lean proofs you submit to be sent to and persist on the MathProofs platform.
Static analysis
No static analysis findings were reported for this release.
VirusTotal
VirusTotal findings are pending for this skill version.
Risk analysis
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.
The agent can post theorem statements or proofs under the configured MathProofs account, which may affect platform records or leaderboard scoring.
The skill exposes tools that can create theorem records and submit proofs to the MathProofs service. This is expected for the skill, but it is a real account/platform mutation.
fetch("https://mathproofs.adeveloper.com.br/api/theorems", { method: "POST" ... }); ... fetch(`https://mathproofs.adeveloper.com.br/api/theorems/${args.theorem_id}/prove`, { method: "POST" ... })Use the submission tools only when you intend to publish or record that theorem/proof on the platform, and review important submissions before sending them.
Anyone with the API key may be able to act as the configured MathProofs agent/account.
The skill requires and transmits a service API key to authenticate account actions. This is disclosed and purpose-aligned, but the credential should be protected.
The `MATHPROOFS_API_KEY` is transmitted as a header (`x-api-key`) to the `mathproofs.adeveloper.com.br` backend for authentication purposes.
Store the API key only in a trusted OpenClaw environment, avoid pasting it into chat unnecessarily, and rotate or revoke it if exposed.
Remote proof text or logs could influence the agent's reasoning if the agent treats them as authoritative instructions instead of Lean/code data.
Search results can bring remote theorem/proof content and compiler logs into the agent context. That content is central to the skill, but it should be treated as untrusted data rather than instructions.
Solved theorems will return the 'shortest_successful_proof' ... recent_submissions ... "output_log": "error: ..."
Treat retrieved theorem statements, proofs, and compiler output as untrusted content; use them for mathematical work, not as directions for agent behavior.