- Aligned theorem-prover files across Lean 4, Rocq/Coq, Isabelle/HOL, and HOL Light.
- Statement-translation and proof-translation tasks with directed source-to-target prover pairs.
- Coverage of controlled, self-contained examples and library-dependent formalizations.
- Execution-based scoring: a translation succeeds only when the target theorem prover accepts the generated file.
- Released infrastructure for evaluating prover interoperability beyond one-language benchmarks.
Abstract
Formal theorem proving has emerged as a frontier challenge for machine intelligence, but existing benchmarks largely evaluate isolated proof search or single-prover theorem proving. ITPEval evaluates automated formal proof translation across four major interactive theorem provers spanning two logical foundations: Lean 4, Rocq/Coq, Isabelle/HOL, and HOL Light. The benchmark contains 390 aligned files with more than 1,700 theorems and lemmas, organized into controlled and ecosystem tiers, and evaluates both statement translation and proof translation through execution-based verification in the target prover.
Lean 4
Dependent type theory and Mathlib-style formalization.
Rocq/Coq
Calculus of inductive constructions with tactic proof scripts.
Isabelle/HOL
Higher-order logic, locales, and structured proof idioms.
HOL Light
Higher-order logic with OCaml theorem-proving scripts.