MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
Logic in Computer Science
2025-11-25 v2 Computation and Language
Machine Learning
Programming Languages
Abstract
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: a natural language description, the Lean formalization, and the Isabelle formalization. We conducted our experiment in 3 stages of increasing complexity, from basic one-shot prompting to multi-turn conversations that incorporate feedback from unsuccessful attempts. At each stage, we perform multiple rounds of translation using increasingly advanced models: GPT-4o mini, Claude 3.5 Sonnet, o1 mini, and o1. We successfully translated 478 out of 488 theorems. The dataset is opensource: https://github.com/LLM4Rocq/miniF2F-rocq.
Keywords
Cite
@article{arxiv.2503.04763,
title = {MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study},
author = {Jules Viennot and Guillaume Baudart and Emilio Jesùs Gallego Arias and Marc Lelarge},
journal= {arXiv preprint arXiv:2503.04763},
year = {2025}
}