Minif2f in Rocq: Automatic Translation Between Proof Assistants — A Case Study

While the Minif2f dataset exists for Lean, Isabelle/HOL, and MetaMath, it has not been formalized in Rocq, limiting cross-system comparisons in automated theorem proving. We investigate whether state-of-the-art LLMs can automatically translate formal theorems between proof assistants. Using a three-stage methodology from basic prompting to multi-turn conversations with error feedback, we successfully translated 478 out of 488 theorems (98%) from Minif2f to Rocq. Expert validation of 150 translations confirmed high accuracy, with only three errors. This work provides a complete Rocq formalization of Minif2f and demonstrates the viability of LLM-based cross-proof-assistant translation.