Lean Formalization

Formalize the requested mathematics without changing the theorem to make the code easier. Treat successful translation as useful mathematical progress, and keep analytical research moving on complete proofs while formalization proceeds separately.

Establish the statement and environment

• Record the original statement, definitions, hypotheses, quantifiers, and conclusion. Map these to the Lean declaration, including implicit arguments, typeclasses, domains, and conventions. For an equivalent formulation, supply the equivalence argument.
• Inspect the project's lean-toolchain, Lake configuration, dependency lockfile, existing modules, and conventions. Use that environment and its exact versions. Check the tools actually available; do not install or upgrade Lean, mathlib, or an MCP server without authorization.
• Search the existing project and its libraries before proving a standard fact again. Cite the reused declaration and verify that its hypotheses match. Use available Lean-LSP tools for goals, diagnostics, or library search; otherwise use the project's Lean/Lake commands. An MCP connection is optional.

Work on the decisive obligations

Choose a small load-bearing lemma or requested theorem. Preserve the source proof's structure where useful, but use idiomatic library arguments rather than translating every prose sentence into a tactic. Temporary sorry placeholders can expose the remaining goals during development; label the file as incomplete and remove them from the target's dependency closure before claiming completion.

Never add the target, an equivalent conjecture, or the missing decisive lemma as an axiom to finish the task. Do not silently strengthen assumptions, specialize a universal theorem to finite cases, or substitute a different definition with the same printed name. If a requested statement is false, show the obstruction and propose an explicitly changed theorem.

Distinguish a missing library lemma, an elaboration problem, and a missing mathematical argument. Resolve concrete formal obstacles with a bounded next step. A stalled formalization does not revoke a complete analytical proof; a substantive counterexample or logical gap does justify reopening that proof.

Once one coherent proof change is ready, run the narrow relevant project check and inspect diagnostics. Pass the exact declaration, statement mapping, environment, and target dependencies to lean-verification when formal assurance is requested. Compilation alone is not that assurance.

Deliver and continue

State what is now formalized and why it matters. Report the exact remaining goals if incomplete, with a useful next action rather than a blanket inability claim. Use established analytical lemmas immediately within their proved scope; do not require external acceptance or whole-manuscript formalization before further research.

Use the formalization handoff when delegating a translation. Read Lean assurance when checking formal completion or interpreting tool limitations. Respect pauses: save the target declaration and unresolved goals, and start no new formalization campaign.