OpenMath Open Theorem

Instructions

Query the OpenMath library to discover and scaffold open theorems. The discovery scripts use OPENMATH_SITE_URL and OPENMATH_API_HOST when set, and otherwise fall back to the default production endpoints.

First-run gate

Before discovery on a new machine or workspace, check the shared openmath-env.json. Auto-discovery only checks ./.openmath-skills/openmath-env.json and ~/.openmath-skills/openmath-env.json.

This gate is mandatory. If openmath-env.json is missing, or if it exists but preferred_language is missing, stop. Do not query the OpenMath theorem list, theorem detail, or download APIs until setup is complete.

If no config exists, stop and ask the user where to create it, then collect at least:

• preferred_language: lean or rocq
• config visibility / save scope: ./.openmath-skills or ~/.openmath-skills
• the submit/authz fields only if the user wants end-to-end submission later

Command: