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.