formalize-informal-proof - SKILL.md Agent Skill

name: formalize-informal-proof description: Convert an informal mathematical proof into verified Lean 4 code. Triggers on "formalize", "convert to Lean", "make rigorous", "verify this proof", or when user pastes informal proof text

Formalize Informal Proof

Convert natural language or textbook proofs into verified Lean 4 code.

Step 1: Parse the Informal Proof

Identify the theorem statement
List each logical step
Identify implicit assumptions
Flag gaps or "clearly/obviously" claims

Create a step map:

Step	Informal	Implicit assumptions
1	"Let x be..."	x exists
2	"Then clearly..."	[needs justification]
...	...	...

Step 2: Identify Required Imports

Based on concepts used:

Number theory → Mathlib.NumberTheory.*
Algebra → Mathlib.Algebra.*
Analysis → Mathlib.Analysis.*
Combinatorics → Mathlib.Combinatorics.*

Step 3: Write Lean Structure

import Mathlib

-- State the theorem
theorem name (hypotheses) : conclusion := by
  -- Step 1: ...
  sorry
  -- Step 2: ...
  sorry

Tools to use:

lean_prover: Verify structure compiles

Step 4: Fill Each Step

For each informal step:

Identify the Lean tactic equivalent
Check if Lean accepts it
If error: add intermediate lemmas

Informal	Lean tactic
"Let x = ..."	`let x := ...` or `obtain ⟨x, hx⟩ := ...`
"Assume P"	`intro h` (if goal is P → Q)
"By definition"	`rfl` or `unfold ...`
"By arithmetic"	`ring` or `omega` or `linarith`
"By induction"	`induction n with k ih`
"Clearly"	`simp`, `trivial`, or needs actual proof

Step 5: Handle Gaps

When the informal proof says "clearly" or "obviously":

Try automated tactics: simp, ring, omega, decide
If fails: This is a real gap
Either find the proof or report to user

Step 6: Validate Complete Proof

No sorry remains
Proof compiles clean
Add comments linking to informal steps

Output Format

**Formalization Report**

**Original theorem:** [as stated informally]

**Formalized statement:**
```lean
theorem ...

Step-by-step translation:

Informal step	Lean tactic	Notes
...	...	...

Complete Lean proof:

[full annotated code]

Gaps found: [if any]

[description of gap and how it was resolved]


## Common Challenges

| Challenge | Solution |
|-----------|----------|
| "WLOG" (without loss of generality) | `wlog` tactic or explicit case split |
| "By symmetry" | `symm` or prove both directions |
| Implicit type coercions | Add explicit casts |
| "Sufficiently large N" | Use `Filter.Eventually` |