OpenMath Lean Theorem

Instructions

Set up the Lean proving environment, validate toolchains, and prove downloaded OpenMath theorems locally. Assumes the theorem workspace was already created by the openmath-open-theorem skill.

Workflow checklist

• Environment: Verify lean, lake, and elan are installed and match the workspace lean-toolchain.
• External skills: Install required Lean proof skills from leanprover/skills. Preferred manual install:

  npx leanprover-skills install lean-proof
  npx leanprover-skills install mathlib-build
  

  If you use preflight auto-install, pass an explicit target such as --install-dir .codex/skills or --install-dir .claude/skills so the write location is deliberate.
• Preflight: Run python3 scripts/check_theorem_env.py <workspace> (see references/preflight.md).
• Prove: Use lean-proof / mathlib-build skills to complete the proof. See references/proof_playbook.md for the OpenMath-specific proving loop.
• Verify: Confirm lake build -q --log-level=info passes and no sorry remains.
• Submit: Use the openmath-submit-theorem skill to hash and submit the proof.