cx-formal-theorem-proving

name	cx-formal-theorem-proving
description	Formalize mathematical statements and produce auditable kernel-check receipts in an existing Lean 4 workspace. Use for theorem-statement audits, proof repair, definition design, tactic or term proofs, dependency minimization, axiom inspection, and correspondence checks between formal and informal claims.

Cx Formal Theorem Proving

Use this Codex adapter for the pinned upstream scientific skill.

Catalog status

• Status: active
• Source: cx
• Audit reasons: none
• Upstream license: MIT
• Inventory: ../../inventory.json
• Upstream instructions: ../../../authored-skills/formal-theorem-proving/SKILL.md

Procedure

1. Resolve the plugin root as three directories above this skill directory.
2. Read the matching inventory record and verify its status, reasons, source path, and pinned revision.
3. Read the upstream instructions only after confirming this record is still active in the current inventory.
4. Treat upstream frontmatter as source metadata, not as Codex configuration. Follow the instruction body only where it is compatible with available Codex tools and the current user-approved plan.
5. Treat tools named for another agent runtime as capability requests. Map them to an available Codex tool only when the behavior is equivalent; otherwise report the unavailable capability.
6. Ask before credentials, package installation, new network hosts, remote compute, writes, paid services, destructive actions, or imported executable code.
7. Use $science-provenance for produced scientific outputs and $science-review before presenting scientific claims.

Boundaries

• This wrapper does not grant credentials, network access, package installation, or script execution.
• Do not change an inactive record to active from inside a research task.
• Preserve failures, uncertainty, source identifiers, and licensing constraints.