Skills openmath-submit-theorem

Name: openmath-submit-theorem
Author: openclaw

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 the Shentu network.

install

source · Clone the upstream repo

git clone https://github.com/openclaw/skills

Claude Code · Install into ~/.claude/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/openclaw/skills "$T" && mkdir -p ~/.claude/skills && cp -r "$T/skills/bennyzhe/openmath-submit-theorem" ~/.claude/skills/openclaw-skills-openmath-submit-theorem && rm -rf "$T"

OpenClaw · Install into ~/.openclaw/skills/

T=$(mktemp -d) && git clone --depth=1 https://github.com/openclaw/skills "$T" && mkdir -p ~/.openclaw/skills && cp -r "$T/skills/bennyzhe/openmath-submit-theorem" ~/.openclaw/skills/openclaw-skills-openmath-submit-theorem && rm -rf "$T"

manifest: skills/bennyzhe/openmath-submit-theorem/SKILL.md

OpenMath Submit Theorem

Instructions

Use this skill for the two-stage Shentu proof submission flow.

Stage 1 submits a proof hash as a commitment so others can see you already know the answer without learning the proof details.
Stage 2 submits the proof detail to reveal and verify the same proof on-chain.
This is an operational skill, not an instruction-only note: it shells out to trusted local
```
python3
```
and
```
shentud
```
, reads shared
```
openmath-env.json
```
, queries/broadcasts to a Shentu RPC endpoint, and uses the local OS keyring for signing flows.
Default: authz + feegrant from
```
prover_address
```
(the user's OpenMath Wallet Address).
Shared config resolution order:
```
--config <path>
```
→
```
OPENMATH_ENV_CONFIG
```
→
```
./.openmath-skills/openmath-env.json
```
→
```
~/.openmath-skills/openmath-env.json
```
. If
```
OPENMATH_ENV_CONFIG
```
is set, treat it as the selected config path. If that file is missing or invalid, stop and fix it instead of silently falling back.
Shentu chain/RPC settings come from
```
SHENTU_CHAIN_ID
```
and
```
SHENTU_NODE_URL
```
or built-in defaults, not from
```
openmath-env.json
```
.
The skill always uses
```
--keyring-backend os
```
for local key lookups and generated submission commands.
Direct signer fallback:
```
generate_submission.py --mode direct
```
.

Required local dependencies are

python3

and

shentud

. Environment variables are optional overrides, not mandatory setup:

OPENMATH_ENV_CONFIG

OPENMATH_SHENTUD_BIN

OPENMATH_SUBMISSION_MODE

OPENMATH_INNER_TX_FEES

OPENMATH_INNER_TX_GAS

SHENTU_CHAIN_ID

, and

SHENTU_NODE_URL

For least-privilege operation, treat

openmath-env.json

creation or editing,

shentud

installation, and local key creation or recovery as manual prerequisites documented in

references/

. The default skill flow may run read-only checks such as

command -v shentud

shentud version

, or

shentud keys show

, but it should not auto-install binaries, auto-edit config files, or run

shentud keys add

as part of normal execution.

Before any action that writes

openmath-env.json

or creates or recovers a local key, get explicit user approval.

shentud

installation should stay a manual user step, guided by the reference docs rather than performed by the skill. Prefer the official Shentu releases page plus a user-local install at

$HOME/bin/shentud

, and use

OPENMATH_SHENTUD_BIN

only as an explicit fallback. Do not generate or manage mnemonics on the user's machine without that approval.

First-run gate

If the selected

openmath-env.json

is missing, or if it exists but is missing

prover_address

agent_address

, or

agent_key_name

, do not proceed. Follow references/init-setup.md, and treat any config write or key creation/recovery as an explicit-user-approval step, then validate:

python3 scripts/check_authz_setup.py [--config <path>]

Require

Status: ready

before any submission. Repeat on each new machine or workspace.

This gate is mandatory for authz-mode scripts that advance the submission flow.

generate_submission.py

must not produce authz

proof-hash

proof-detail

commands until

check_authz_setup.py

returns

Status: ready

. Read-only status polling via

query_submission_status.py

is exempt.

Workflow checklist

Manual prerequisites: If
```
shentud
```
is missing, use
```
references/submission_guidelines.md
```
for manual binary install. If
```
openmath-env.json
```
is missing or incomplete, or the local
```
os
```
key does not exist yet, use
```
references/init-setup.md
```
. If authz or feegrant is still missing after setup, use
```
references/authz_setup.md
```
. The default skill flow should not auto-edit config files, auto-install
```
shentud
```
, or auto-create or recover keys.

Env:

openmath-env.json

exists in

./.openmath-skills/

~/.openmath-skills/

, and

check_authz_setup.py

reports

Status: ready

Stage 1 (Commit): Run

generate_submission.py hash <theoremId> <proofPath> <proverKeyOrAddress> <proverAddr>

only after the first-run gate passes; this generates the commitment hash and the corresponding

shentud tx authz exec proofhash.json ... --fee-granter <prover-address>

flow.

Wait: 5–10 s, then

query_submission_status.py tx <txhash> --wait-seconds 6

. Confirm proof in

PROOF_STATUS_HASH_LOCK_PERIOD

and record

proof_id

Stage 2 (Reveal): Run
```
generate_submission.py detail <proofId> <proofPath> <proverKeyOrAddress>
```
only after the first-run gate passes; this reveals the proof detail and emits the corresponding
```
shentud tx authz exec proofdetail.json ... --fee-granter <prover-address>
```
flow. Do not wait for hash lock expiry.

Verify: Wait 5–10 s, then

query_submission_status.py theorem <theoremId> --wait-seconds 6

. Confirm theorem reaches

THEOREM_STATUS_PASSED

Scripts

Script	Command	Use when
Authz readiness	`python3 scripts/check_authz_setup.py [--config <path>]`	Before first submission and when changing env; validates CLI, keys, RPC, authz, feegrant.
Stage 1 commands	`python3 scripts/generate_submission.py hash <theoremId> <proofPath> <proverKeyOrAddress> <proverAddr>`	Generating `proofhash.json` and the broadcast command for the commitment stage. In authz mode, refuses to continue until the first-run gate passes.
Stage 2 commands	`python3 scripts/generate_submission.py detail <proofId> <proofPath> <proverKeyOrAddress>`	Generating `proofdetail.json` and the broadcast command for the reveal stage (use `proof_id` from Stage 1). In authz mode, refuses to continue until the first-run gate passes.
Query tx	`python3 scripts/query_submission_status.py tx <txhash> [--wait-seconds 6]`	After broadcast to confirm inclusion.
Query theorem	`python3 scripts/query_submission_status.py theorem <theoremId> [--wait-seconds 6]`	Final status check.
Proof hash (debug)	`python3 scripts/calculate_proof_hash.py <theoremId> <proverAddress> <proofContentOrFile>`	Standalone hash check; normally used by generate_submission.

submission_config.py

loads and validates only the identity/authz fields in

openmath-env.json

using the shared config resolution order above. Chain/RPC settings come from

SHENTU_CHAIN_ID

and

SHENTU_NODE_URL

Reference split:

```
references/submission_guidelines.md
```
: manual binary install, pre-submission checks, and the two-stage submit flow
```
references/init-setup.md
```
:
```
openmath-env.json
```
, local key setup, and the normal website authorization flow
```
references/authz_setup.md
```
: manual authz + feegrant CLI fallback after setup

Notes

Authz: Default flow uses

shentud tx authz exec

with

--fee-granter <prover-address>

. For direct signer use

--mode direct

generate_submission.py

Commit-reveal: Stage 1 publishes only the proof hash as a commitment, which reduces proof leakage and front-running risk while reserving your claim. Stage 2 reveals the full proof detail for verification.
Key material: Treat local key creation or recovery as a manual step. If
```
shentud keys add
```
is needed, show the user the documented commands in the references instead of running them from the skill, and warn that mnemonics or recovery material may be shown.
Binary setup: Manual binary setup is required. Prefer a trusted release binary installed at
```
$HOME/bin/shentud
```
. Verify with
```
command -v shentud
```
and
```
shentud version
```
before submission.
Config editing: Manual config setup is preferred. Point the user to
```
references/init-setup.md
```
and
```
references/openmath-env.example.json
```
instead of having the skill rewrite
```
openmath-env.json
```
.
Binary resolution: Check the plain
```
shentud
```
command first. If
```
shentud
```
already works from
```
PATH
```
, do not force a separate binary path. Set
```
OPENMATH_SHENTUD_BIN
```
only as a fallback when the default
```
shentud
```
lookup is missing or broken and you need a specific trusted binary.

Advanced env vars:

OPENMATH_SUBMISSION_MODE

changes the default

generate_submission.py --mode

(

authz

by default).

OPENMATH_INNER_TX_FEES

and

OPENMATH_INNER_TX_GAS

override the generated inner

--generate-only

tx fees/gas in authz mode.

Local shell env:
```
PATH
```
affects local
```
python3
```
/
```
shentud
```
discovery, and references may use
```
$HOME/bin
```
when showing non-persistent local install examples.
Block wait: After each broadcast wait ~5–10 s before querying.

References

Load when needed (one level from this file):

references/init-setup.md — Config-first env setup, local key resolution, and the normal website authorization flow.
references/openmath-env.example.json — Template for
```
openmath-env.json
```
.
references/submission_guidelines.md — Manual binary install, pre-submission checks, commit-reveal execution, and status verification.
references/authz_setup.md — Manual authz grants and feegrant fallback after setup.