openmath-submit-theorem

Submits proofs to the OpenMath platform using a two-stage commit-reveal flow. Use when the user wants to commit a proof hash or reveal a Lean/Rocq proof on t...

What to check before installing/using this skill: - Review the included scripts locally (they are plain Python and readable). They call the local shentud CLI and use subprocess to run it; the scripts do not download remote code or auto-install binaries. - Verify the shentud binary you use: follow the official Shentu releases page and install a vetted binary to $HOME/bin/shentud or set OPENMATH_SHENTUD_BIN to an absolute path you trust. Do not point this to a binary from an untrusted source. - Understand key access: the skill relies on shentud --keyring-backend os to read/use local keys. That means the CLI (not these scripts) will access keys in your OS keyring when you run signing commands. Do not run these scripts on a machine where private keys are exposed or where you don't want the agent to be able to invoke shentud commands. - Config file safety: openmath-env.json contains addresses and config. Keep it in a location you control (project or user path). If you set OPENMATH_ENV_CONFIG to point to a file, ensure it is a file you trust — the skill treats that as authoritative and will stop on missing/invalid files. - Operational caution: the skill prints and generates shentud txs and may run shentud queries. It enforces a 'first-run gate' and does not auto-broadcast inner txs in authz mode (it generates JSON and prints the shentud tx authz exec command). Still, be careful when broadcasting transactions and ensure the prover/fee-granter addresses and amounts are correct. - If you allow the agent autonomous invocation, know that it could run the readiness checks and any shentud commands permitted by your local keyring and authz grants. That is expected for an agent that can perform submissions, but review and limit autonomous permissions if you are concerned. If you want an extra safety step: run the scripts manually in a sandboxed or test environment first (no real keys, or use a testnet key) to observe behavior before using production keys or balances.