# ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 43 references that are in the map.
- First posted on arXiv 7 Jul 2026.

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

- [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)
- [CodeGeeX: A Pre-Trained Model for Code Generation with Multilingual Benchmarking on HumanEval-X](https://mlsanity.com/paper/2303.17568/) (2023)
- [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)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [CodeTransOcean: A Comprehensive Multilingual Benchmark for Code Translation](https://mlsanity.com/paper/2310.04951/) (2023)
- [Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency](https://mlsanity.com/paper/2410.20936/) (2024)
- [CRUXEval-X: A Benchmark for Multilingual Code Reasoning, Understanding and Execution](https://mlsanity.com/paper/2408.13001/) (2024)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries](https://mlsanity.com/paper/2504.19110/) (2025)
- [MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study](https://mlsanity.com/paper/2503.04763/) (2025)
- [ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving](https://mlsanity.com/paper/2502.04671/) (2025)
- [KELPS: A Framework for Verified Multi-Language Autoformalization via Semantic-Syntactic Alignment](https://mlsanity.com/paper/2507.08665/) (2025)
- [TransLibEval: Demystify Large Language Models' Capability in Third-party Library-targeted Code Translation](https://mlsanity.com/paper/2509.12087/) (2025)

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

- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)

## Abstract (arXiv)

Formal theorem proving has emerged as a frontier challenge for machine learning, yet the ecosystem is fragmented: proofs remain siloed across incompatible systems, limiting both training data for learning-based provers and the portability of verified results. We present ITPEval, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations. Our benchmark comprises 1,560 source files and 6,848 theorems organized into a controlled tier of axiomatized files that isolates foundational translation difficulty, and an ecosystem tier drawn from real libraries that exposes API and proof-style mismatches. We release itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics. We evaluate both statement and proof translation across five frontier and open-weight LLMs on 12 directed translation pairs: statement translation peaks at 29.1% pass@1 and proof translation at 10.5%; controlled theorems reach 29.7% proof pass@1 versus 5.2% for ecosystem-level translations, confirming that library mismatch is the dominant bottleneck. In addition to pass@k evaluation, a deterministic Lean 4 BEq check establishes equivalence for 54.0% of verified source-to-Lean 4 miniF2F statement translations, showing that native type-checking alone can substantially overestimate semantic fidelity; in an autoformalization/auto-informalization round-trip study, Rocq and HOL Light are easier formalization targets than Lean 4 and Isabelle, while multi-ITP context improves pooled Lean 4 success from 4.8% to 10.6%. Our benchmark, verification infrastructure, and evaluation pipelines are publicly released.