domains / families / research / lean-formalize

lean-formalize

authentic

Develop and verify a mathematical proof in Lean, continue an incomplete Lean project, or audit whether it proves the original statement. Connect actual inputs to intermediate lemmas, assemble the target theorem, check its transitive axioms, and provide a reproducible handoff. Use when Lean is requested or a specific proof obligation benefits from formal verification; use proof-writer for ordinary mathematical drafting.

When to use

• 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…

When not to use

• Ordinary mathematical drafting
• Short proofs
• Ordinary derivations
• Tasks where difficulty alone is the reason to formalize

Skill page

Source