lean-interact: Skill for Claude Code

formalize

The core loop of this repository. The user — a working mathematician who knows the mathematics and is learning Lean — types a sentence of ordinary mathematics; you return compiled Lean plus a short teaching note.

Repository root: /path/to/lean-interact, the directory this clone lives in. Use absolute paths when reading and editing files. Run the tools/ scripts from the repository root with repo-relative paths (python3 tools/mlq.py …): that is the form .claude/settings.json allows without a permission prompt, and it is the form to show the user.

Before the first formalization of a session, read MEMORY.md and vault/Formalization Style.md. They contain decisions you would otherwise contradict.

Run the steps in order. Do not skip steps because the claim looks easy; the cheap steps are the ones that prevent the expensive mistakes.

---

Step 1 - UNDERSTAND

Restate the claim as precise mathematics before touching any file. Make explicit, in one short paragraph:

• every quantifier and its range;
• every hypothesis, including the ones ordinary prose leaves silent (p prime often means odd; "a/b" often means b ∣ a; "the order of a" presupposes gcd(a, n) = 1);
• the ambient type.

Choose the ambient type using vault/Nat vs Int vs ZMod.md. If that note is not present yet, use the table in vault/Formalization Style.md section 1. The short version:

The claim is about	Type
counting, divisibility, gcd, primes, no subtraction	ℕ, with Nat.ModEq for congruences
genuine differences, negatives, Bezout coefficients	ℤ, with Int.ModEq
a fixed numeral modulus, ring or unit structure mod n, squares, orders	ZMod n
a quantified modulus n	Nat.ModEq / Int.ModEq, never ZMod n (dependent type pain)

Ambiguity rule. Ask at most ONE short question, and only if the answer would change the statement. Otherwise state the assumption in one clause and continue: "Taking n > 0 and a coprime to n; say if you meant otherwise." Never open a formalization with a list of questions.