APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries
Abstract
While frontier formal mathematics systems now routinely develop repository-scale proof engineering artifacts requiring multi-file coordination and semantic correctness beyond compilation, existing evaluation benchmarks remain focused on isolated theorem proving. We introduce Automated Proof Engineering (APE), the first systematic framework for evaluating repository-scale proof engineering through dual verification that validates both syntactic compilation and semantic requirement satisfaction in pinned library environments. We present a complete infrastructure comprising APE-Bench, which automatically extracts proof engineering tasks from real library commit histories, and APE-Harness, a unified execution framework based on task contract abstraction. This contract-based design enables standardized evaluation across diverse formal mathematics tasks and fair systematic comparison of different agent implementations (including our APE-Agent reference scaffold alongside Claude Code and Codex CLI) on identical task specifications. We demonstrate the framework's effectiveness through comprehensive evaluation. All code and benchmark dataset are released as open-source at https://github.com/xinhjBrant/APE-Bench.
Cite
@article{arxiv.2504.19110,
title = {APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries},
author = {Huajian Xin and Luming Li and Xiaoran Jin and Jacques Fleuriot and Wenda Li},
journal= {arXiv preprint arXiv:2504.19110},
year = {2026}
}