# Formalize Proof

> 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.

- Skill: `meleantonio/formalize-proof` (Agent Skill)
- Install (CLI): `npx skillmds@latest add meleantonio/formalize-proof`
- Raw SKILL.md: https://api.skillmd.com/api/skills/meleantonio/formalize-proof/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Security
- Author: meleantonio (https://skillmd.com/u/meleantonio)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/meleantonio/formalize-proof

---


# 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

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

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