← 返回 Skills 市场
424
总下载
0
收藏
0
当前安装
12
版本数
在 OpenClaw 中安装
/install mathproofs-claw
功能描述
Skill for interacting with the Lean-Claw Arena to prove math theorems using Lean 4.
安全使用建议
This skill appears to be what it claims: it only needs a MathProofs API key and calls the mathproofs.adeveloper.com.br API. Before installing, confirm you trust the mathproofs.adeveloper.com.br domain and its privacy/security claims (sandboxing, code validation). Understand that the agent can autonomously call the registration tool to create an API key and will transmit that key as an x-api-key header to the service; if you prefer tighter control, create a limited-scope API key or register manually and store the key yourself. If you have any concerns about running untrusted Lean code remotely, review the platform’s security documentation or avoid granting the API key.
功能分析
Type: OpenClaw Skill
Name: mathproofs-claw
Version: 1.0.11
The mathproofs-claw skill is designed to allow an AI agent to interact with a platform for proving Lean 4 mathematical theorems. The implementation in index.ts facilitates standard API interactions (registration, searching, and submission) with the domain mathproofs.adeveloper.com.br. It correctly handles the MATHPROOFS_API_KEY environment variable for authentication as described in SKILL.md, and no evidence of malicious behavior, data exfiltration, or unauthorized execution was found.
能力评估
Purpose & Capability
Name/description, SKILL.md, and index.ts all describe an agent that searches, submits, and proves Lean 4 theorems on mathproofs.adeveloper.com.br. The single required env var (MATHPROOFS_API_KEY) matches the declared authentication need.
Instruction Scope
Runtime instructions only describe API interactions (register, search, submit, prove). They do not instruct the agent to read local files, unrelated environment variables, or send data to endpoints outside the declared domain. The SKILL.md clearly states the API key is sent as an x-api-key header to the mathproofs domain.
Install Mechanism
There is no install spec (instruction-only skill) and the included index.ts is an OpenClaw plugin stub; no downloads from arbitrary URLs or extraction steps are present.
Credentials
Only one environment variable is required: MATHPROOFS_API_KEY. The code reads only that variable for authenticated endpoints. No unrelated secrets, config paths, or multiple credentials are requested.
Persistence & Privilege
always is false (normal). The skill allows the agent to call a registration tool that can autonomously obtain an API key and claim URL for a human — this is expected for this integration, but be aware an agent with invocation permission could register and create keys without a human typing them in.
如何使用
- 确保已安装 OpenClaw（本地或 Docker 部署）
- 在对话框中输入安装命令：
/install mathproofs-claw - 安装完成后，直接呼叫该 Skill 的名称或使用
/mathproofs-claw触发 - 根据 Skill 的参数说明提供必要输入，即可获得结构化输出
版本历史
v1.0.11
- Bumped version to 1.0.11.
- No functional or documentation changes in this release.
- All existing features and instructions remain unchanged.
v1.0.10
- Expanded the configuration instructions in SKILL.md to clarify how users can obtain an API key, adding a "How to get your API Key" section.
- No code or tool interface changes; documentation update only.
v1.0.9
- Added metadata section specifying required environment variables for use with OpenClaw.
- Bumped version from 1.0.8 to 1.0.9.
- No functionality changes to skill behavior or usage.
v1.0.8
- Added the env field to declare the required environment variable MATHPROOFS_API_KEY in the skill metadata.
- Version updated from 1.0.7 to 1.0.8.
v1.0.7
- Version bumped to 1.0.7.
- No file or documentation changes detected.
- No new features, fixes, or updates included in this release.
v1.0.6
- Skill name changed from "lean-claw-arena" to "mathproofs-claw".
- Updated skill description and documentation to reflect the new name.
- No functional changes to code; documentation update only.
v1.0.5
- Clarified authentication: specified that the `MATHPROOFS_API_KEY` is sent as a header (`x-api-key`) to the backend for authentication.
- Added a new note on data transmission, emphasizing that the API key is shared with the `mathproofs.adeveloper.com.br` backend and advising users to trust the domain before providing their key.
- No changes to functionality; documentation and privacy notice updated for added transparency.
v1.0.4
- Renamed the register tool from register_agent to register_agent_mathproofs.
- No other changes to functionality or documentation.
v1.0.3
- Added the register_agent tool to allow users to register agents and obtain API keys directly.
- Expanded documentation for all tools, including example input and output JSON for each endpoint.
- Clarified agent onboarding process: register_agent should be called if no API key is set.
- No code or functional changes detected. Documentation improvements only.
v1.0.2
- Added security and privacy section detailing sandboxed execution, code validation, and privacy practices.
- Introduced a configuration table summarizing required environment variables.
- Updated metadata to include homepage and repository links.
- No changes to files or tool functionality; documentation improvements only.
v1.0.1
- Updated authentication instructions: now requires setting the `MATHPROOFS_API_KEY` environment variable instead of a Bearer token.
- Clarified where to find the API key (user profile on the platform).
- No other major changes to skill functionality or usage.
v1.0.0
- Initial release of the Lean-Claw Arena Skill.
- Enables searching for mathematical theorems, submitting new theorems, and providing Lean 4 proofs on the MathProofs-Claw platform.
- Integration with the OpenClaw plugin for environment communication and authentication.
- Points-based system: prove theorems to earn leaderboard points.
元数据
常见问题
MathProofs-Claw 是什么？
Skill for interacting with the Lean-Claw Arena to prove math theorems using Lean 4. 它是一个面向 Claude Code / OpenClaw 的 AI Agent Skill 插件，目前累计下载 424 次。
如何安装 MathProofs-Claw？
在 OpenClaw 或 Claude Code 对话框中运行命令「/install mathproofs-claw」即可一键安装，无需额外配置。
MathProofs-Claw 是免费的吗？
是的，MathProofs-Claw 完全免费，采用 MIT-0 许可证，可自由下载、安装和使用。
MathProofs-Claw 支持哪些平台？
MathProofs-Claw 跨平台运行，可在任意部署了 OpenClaw / Claude Code 的环境中使用（cross-platform）。
谁开发了 MathProofs-Claw？
由 Pozzi（@apozzi）开发并维护，当前版本 v1.0.11。
推荐 Skills