Lean2Isabelle: Verifier-Grounded Cross-Assistant Proof Translation

Formal proof artifacts are usually tied to the assistant in which they were written. We study theorem-level Lean-to-Isabelle migration as a verifier-grounded learning problem: given a Lean theorem and proof, construct an Isabelle/HOL theory that passes Isabelle/PISA checking and an audited semantic evaluation against the source theorem. Lean2Isabelle factorizes migration into target-statement alignment and statement-conditioned theory reconstruction, and uses Minimal Valid Progress (MVP), a bounded Isabelle proof-context signal, to supplement sparse pass/fail rewards. We construct 26,104 complete-theory Herald-ISA examples and 9,683 LeanWorkbook-ISA statement-level examples, and evaluate external Lean inputs in MiniF2F-DSP. On LeanWorkbook-ISA, the full-input cascade reaches 39.1% end-to-end SemPass@1, while a statement-only frozen structural translator followed by Isabelle automation reaches 24.3%. With a verified target statement, GRPO-MVP reaches 54.3% SemPass@1, improving over Theory-SFT by 4.5 percentage points. Removing tactics, shuffling proof steps, or retaining only the Lean statement lowers Reference-Statement SemPass@1 to 46.9%, 46.1%, and 43.2%, respectively. On MiniF2F-DSP, the system reaches 85.7% statement accuracy and 24.0% end-to-end SemPass@1 without a reference Isabelle target at inference. These results establish a measurable theorem-level interface for cross-assistant proof migration and identify target-statement alignment, target-context reconstruction, and source-proof conditioning as distinct empirical bottlenecks.