| 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
- Install/toolchain check (
lake, mathlib as needed). Do not assume the
user already has Lean.
- Formalize the main theorem statement first; freeze it.
- Set a small
/goal (or equivalent): formalize one lemma or section.
- Expand the goal only after the small piece compiles.
- 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.
- 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.
