arxivcs.AIcs.LO2026-07-07
ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers
Jiayi Wu, Robert Joseph George, Anima Anandkumar
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,…