MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study

Jules Viennot, Guillaume Baudart, Emilio Jesùs Gallego Arias +1

In this work, we conduct an experiment using state-of-the-art LLMs to translate MiniF2F into Rocq. The translation task focuses on generating a Rocq theorem based on three sources:…