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

arXiv: https://arxiv.org/abs/2503.04763 · HTML: https://mlsanity.com/paper/2503.04763/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 14 references that are in the map.
- First posted on arXiv 11 Feb 2025.

## Builds on (most cited first, 12 of 12)

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)
- [A Survey on Pretrained Language Models for Neural Code Intelligence](https://mlsanity.com/paper/2212.10079/) (2022)

## Built on by (most cited first, 5 of 5)

- [Agentic Proving for Program Verification](https://mlsanity.com/paper/2605.23772/) (2026)
- [ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers](https://mlsanity.com/paper/2607.19407/) (2026)
- [Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP](https://mlsanity.com/paper/2603.20405/) (2026)
- [PPDL: LLM-Based Flows as Probabilistic Programs](https://mlsanity.com/paper/2608.05234/) (2026)
- [Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean](https://mlsanity.com/paper/2609.39544/) (2026)

## Abstract (arXiv)

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.