Jacques Fleuriot

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 Engineer…