lean-interact: Skill for Claude Code

formalize-from-magma

The second input path of this project. formalize takes a sentence of ordinary mathematics; this skill takes Magma code and turns it into the same thing.

Magma code is not a theorem. It is an algorithm plus evidence. The work is to recover the mathematical claim the code embodies, decide which part of it is actually provable, and only then formalize. Skipping to Lean without running the code is the characteristic mistake: you end up formalizing what you assumed the code did.

Repository root: /path/to/lean-interact. Magma runs remotely — there is no local binary. See magma/README.md.

---

Step 1 - RUN IT, before reading it closely

tools/magma_run.sh path/to/file.m          # a file
echo 'print 2^10 mod 11; quit;' | tools/magma_run.sh -

Read the actual output. Magma's semantics differ from the mental model you bring from Lean or Python in ways that change the claim:

Magma	Trap
n mod m	for negative n, Magma returns a value in [0, m) — like Int.emod, unlike truncation
Modexp(a, e, m)	handles negative a and huge e; do not "simplify" it to a^e mod m in your head
Gcd(0, 0)	0; edge cases at zero are where computational claims quietly fail
[a..b]	empty when a > b, so a sweep can silently check nothing
EulerPhi(1)	1, and 1 mod 1 = 0 — degenerate moduli are the usual source of a false pattern

If the code defines functions but runs nothing, add a driver that exercises them and run that. Never formalize from unexecuted code.

Step 2 - EXTRACT THE CLAIM

Ask what the code asserts, and classify it. The classification decides everything downstream:

1. A closed computation. Modexp(2, 560, 561) eq 1. Formalizes to a concrete Lean statement provable by decide or norm_num. Cheap, honest, and worth keeping when it is a witness or a counterexample.
2. A universally quantified claim, verified on a range. A forall{...} over [1..1000] returning true. The Magma output is evidence, not proof. The Lean statement must quantify over all n, and the proof must be a real argument.
3. A pattern with a hidden hypothesis. The sweep skipped cases (if n mod p ne 0), or the range excluded them ([1..N] hides the negative and zero cases). That skipped condition is the hypothesis of the theorem. This is the most valuable thing this skill finds — see the worked example below.
4. An algorithm. A routine computing something. Formalizing an algorithm means stating its specification; that is a much larger job. Say so, and offer the specification as the claim instead of the implementation.