lean-formalize

Lean Formalize

Turn the user's mathematical statement into a checked Lean theorem with its meaning preserved. A compiled conditional lemma is progress; completion concerns the original statement and the trust basis actually used.

When to use Lean

Use this skill when the user requests Lean, when continuing an existing Lean proof, or when formal verification addresses a concrete uncertainty in a central claim—for example, a long dependency chain, a delicate reduction, or coverage of a finite classification. State the obligation it will help resolve and proceed within the authorized task. Difficulty alone is not a reason to formalize. Ordinary derivations and short proofs can stay in formula-derivation or proof-writer; do not make Lean a prerequisite for every mathematical result. Respect the user's chosen proof method and the scale of the requested work.

Core workflow

Original statement and Lean definitions
  → A: cross-family adversarial statement alignment
  → Proof obligations, representations, and lemma interfaces
  → Lean implementation ↔ B: adversarial review of key arguments and connections
  → Actual inputs connected; original theorem assembled
  → Executed type, definition, and transitive-axiom audit
  → C: cross-family adversarial review of the final exported result
  → Reproducible delivery and research-state update

For substantial new proof projects, A/B/C are part of the workflow. For a continuation, reuse completed checks on unchanged claims and revisit affected ones. Small routine formalizations need checks proportional to the actual claim; an explicit user request for cross-family review still applies to them.

Use the authorized reviewer families available in the current host. If the user specifies both Grok and Gemini, obtain and record both; a same-family agent or another provider does not silently satisfy either request. Unavailability leaves that checkpoint pending while independent proof work continues. A checked theorem and a fully completed requested review workflow are separate deliverables.