Lean2Isabelle: Factorized Cross-Assistant Proof Translation

Formal proofs are spread across proof assistants, but reusing a verified Lean proof in Isabelle/HOL requires more than syntax translation: the target theory must check and preserve the source theorem's meaning under semantic evaluation. We introduce Lean2Isabelle, a verifier-grounded Lean-to-Isabelle proof-translation framework that factorizes the task into target-statement prediction and statement-conditioned Isabelle theory generation. This factorization supports Reference-Statement evaluation, which isolates proof reconstruction with a verified target statement, and Predicted-Statement evaluation, which measures the end-to-end cascade. We construct Herald-ISA and LeanWorkbook-ISA, derive MiniF2F-DSP from public DeepSeek-Prover-V2 miniF2F Lean proofs, and train Statement-SFT, Theory-SFT, and a GRPO proof translator with Isabelle/PISA verifier feedback, Minimal Valid Progress shaping, and a Difficulty-Ordered curriculum. Statement-SFT reaches 86.0% and 85.7% EqStmt@1 on LeanWorkbook-ISA and MiniF2F-DSP; in Reference-Statement proof translation, GRPO-MVP-DifficultyOrdered raises LeanWorkbook-ISA SemPass@1 from 49.8% to 54.3%. In Predicted-Statement translation, the final system reaches 39.1% and 24.0% SemPass@1 on LeanWorkbook-ISA and MiniF2F-DSP, while source ablations lower LeanWorkbook-ISA SemPass@1 to 45.3% without Lean input and 43.2% with a shuffled Lean proof, indicating that matched Lean context carries useful proof signal.