formalize-proof

name	formalize-proof
description	Formalize a natural-language mathematical proof in Lean 4 (or another kernel) incrementally: small goals first, expand, audit mismatches, refactor. Use after an informal proof of an open problem is drafted and audited, or when the user asks for Lean formalization of a proof artifact.

Formalize a proof

Follow-on to a successful informal resolution. Formalization is optional for claiming an informal win, but it is the strongest machine check available.

Incremental strategy

1. Install/toolchain check (lake, mathlib as needed). Do not assume the user already has Lean.
2. Formalize the main theorem statement first; freeze it.
3. Set a small /goal (or equivalent): formalize one lemma or section.
4. Expand the goal only after the small piece compiles.
5. When the agent gets stuck on a tactic hole that hides a math gap, return to natural-language repair (adversarial-proof-audit) before forcing Lean.
6. After a full formalization, refactor for readability and re-check that the formal statement matches the paper’s theorem exactly.

Cross-model audit

If available, use a second coding agent to audit Lean code vs the paper for:

• statement mismatches;
• sorry / admit / unchecked axioms;
• classical vs constructive mismatches that change the claim;
• hidden extra hypotheses in the formal theorem.

Artifacts

problems/<id>/lean/
  lakefile.toml / lakefile.lean
  Main.lean
  ...
  FORMALIZATION_NOTES.md

Record in STATUS.md whether formalization is complete, partial, or pending.