/lean-formalize

name: lean-formalize
description: "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."
argument-hint: "[statement, proof file, Lean project, or audit request]"
allowed-tools: Bash(*), Read, Write, Edit, Grep, Glob, Agent, Skill, mcp__codex__codex, mcp__codex__codex-reply

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.

Scope and entry

Follow the requested scope: implement, continue, audit, or package. For an audit, inspect and report rather than silently repairing or weakening the theorem. For implementation, develop the mathematical argument as well as its Lean proof: search relevant literature or library results, explore alternative routes, and discharge the missing lemmas. Continue through the remaining interfaces and top-level assembly; do not stop at a target declaration or the first successful compilation.

Read the authoritative statement, existing Lean entry point, toolchain and lockfile, and latest progress record. Reuse the project and its document names. Do not reinstall tools, change dependencies, or start a new proof framework when the existing environment is suitable. Resolve APIs against the pinned library.

Use the existing proof route when it works. If the mathematical argument itself is missing, isolate that obligation and use `proof-writer` or ordinary proof work. A delegated `proof-writer` task develops that argument and returns its proof or remaining gap to this run; it must not invoke `lean-formalize` again. Syntax automation cannot discharge an unproved premise. Do not promise that an arbitrary open problem can be formalized or solved.

Start or resume the right work

| Current input | First useful action | |---|---| |Only a mathematical statement|Fix definitions and quantifiers, then develop a proof route and its first difficult obligation| |A prose proof|Identify nontrivial dependencies and choose Lean representations; expose any missing argument before coding it| |A partial Lean project|Inspect the target and its actual callers, read the last useful build/error record, and continue at the highest unclosed connection| |An audit request|Read definitions and exported types, run applicable checks, and report; do not silently repair the target| |A completed proof to hand off|Check the current entry point and evidence, then prepare portable sources and commands without restarting the mathematical search|

Name the intended main module, exported declaration, and current next obligation early. If no complete mathematical route is known, say which statement is being attempted; do not mark it provable merely because the implementation has started. Tool/API problems and missing mathematical arguments require different next steps.

1. Fix meaning before implementation

Record a short mathematical specification, or reference the existing one:

• Objects, domains, quantifiers, original hypotheses, and conclusion.
• Equivalence of convenient representations to the original objects.
• User constraints on computation, external certificates, and logical foundations.
• The Lean declarations intended to express and prove the result.

Separate original hypotheses from properties introduced by a reduction. Identify where finiteness, nonemptiness, decidability, normalization, and index conventions change the statement or require a bridge. Check plausible vacuity and quantifier failures in the actual theorem, rather than inventing unrelated edge cases.

Keep the user's original statement as the comparison baseline until the user changes the goal. A working specification rewritten to match the implementation d