APE-Bench: Evaluating Automated Proof Engineering for Formal Math Libraries

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, benchmarks, and infrastructure will be open-sourced.

AI systems can now prove mathematical theorems, and some have even made substantial contributions to major libraries of computer-verified proofs. But real-world formal mathematics development goes far beyond proving individual theorems—it requires navigating large codebases, coordinating dependencies across files, and maintaining existing proofs as libraries evolve. These everyday engineering activities constitute the bulk of formal mathematics work, yet no systematic way exists to evaluate whether AI can perform them. We introduce Automated Proof Engineering (APE), the first framework for evaluating AI on repository-scale proof engineering. APE-Bench automatically extracts engineering tasks from real library maintenance histories, requiring AI to modify code according to natural-language instructions and pass both compilation and semantic correctness checks. APE-Harness provides a unified execution infrastructure that enables fair comparison of different AI systems on identical tasks under identical conditions. We demonstrate the framework's effectiveness through comprehensive evaluation covering model performance and efficiency analysis, semantic judge reliability validation, comparison across different AI agent implementations, and tool configuration studies. All code, benchmarks, and infrastructure are released as open-source.